Editing Dyadic rational (section)

===Other related constructions===
In [[reverse mathematics]], one way of constructing the [[real number]]s is to represent them as functions from [[Unary numeral system|unary numbers]] to dyadic rationals, where the value of one of these functions for the argument <math>i</math> is a dyadic rational with denominator <math>2^i</math> that approximates the given real number. Defining real numbers in this way allows many of the basic results of [[mathematical analysis]] to be proven within a restricted theory of [[second-order arithmetic]] called "feasible analysis" (BTFA).{{r|fer-fer}}

The [[surreal number]]s are generated by an iterated construction principle which starts by generating all finite dyadic rationals, and then goes on to create new and strange kinds of infinite, infinitesimal and other numbers.{{r|conway}} This number system is foundational to [[combinatorial game theory]], and dyadic rationals arise naturally in this theory as the set of values of certain combinatorial games.{{r|mauldon|flanigan|uit-bar}}

The [[fusible number]]s are a subset of the dyadic rationals, the closure of the set <math>\{0\}</math> under the operation <math>x,y\mapsto(x+y+1)/2</math>, restricted to pairs <math>x,y</math> with <math>|x-y|<1</math>. They are [[well-order]]ed, with [[order type]] equal to the [[Epsilon numbers (mathematics)|epsilon number]] <math>\varepsilon_0</math>. For each integer <math>n</math> the smallest fusible number that is greater than <math>n</math> has the form <math>n+1/2^k</math>. The existence of <math>k</math> for each <math>n</math> cannot be proven in [[Peano arithmetic]],{{r|eri-niv-xu}} and <math>k</math> grows so rapidly as a function of <math>n</math> that for <math>n=3</math> it is (in [[Knuth's up-arrow notation]] for large numbers) already larger than <math>2\uparrow^9 16</math>.{{r|A188545}}

The usual proof of [[Urysohn's lemma]] utilizes the dyadic fractions for constructing the separating function from the lemma.