Rational and real numbers.md (2127B)
1 +++ 2 title = 'Rational and real numbers' 3 +++ 4 # Rational and real numbers 5 ## Rational numbers 6 Rational numbers are fractions. 7 As integers are naturals with a minus operator, rationals are integers with a division operator. 8 9 ```lean 10 structure fraction := 11 (num : Ζ) 12 (denom : Ζ) 13 (denom_ne_zero : denom ≠ 0) 14 ``` 15 16 You can then define equivalence on a fraction: 17 18 ```lean 19 @[instance] def fraction.setoid : setoid fraction := 20 { r := λa b : fraction, num a * denom b = num b * denom a, 21 iseqv := /- proof -/ } 22 23 lemma fraction.setoid_iff (a b : fraction) : 24 a ≈ b ↔ num a * denom b = num b * denom a := 25 by refl 26 ``` 27 28 Then define rationals based on the setoid: 29 30 ```lean 31 def rat : Type := quotient fraction.setoid 32 33 @[instance] def has_zero : has_zero rat := 34 { zero := ⟦0⟧ } 35 36 @[instance] def has_one : has_one rat := 37 { one := ⟦1⟧ } 38 39 @[instance] def has_add : has_add rat := 40 { add := 41 quotient.lift₂ (λa b : fraction, ⟦a + b ⟧) 42 by /- proof -/ } 43 ``` 44 45 Could also use a subtype of `fraction`, but then more complicated function definitions are needed. 46 47 ## Real numbers 48 Some sequences seem to converge, but don't converge to a rational number. For example √2. 49 The reals are rationals with a limit. 50 51 A sequence of rational numbers is Cauchy if for a nonzero `x`, there is an `n ∈ Ν`, such that for all `m ≥ n`, we have `|a_n - a_m| < x`. 52 53 ```lean 54 def is_cau_seq (f : Ν → Q) : Prop := 55 ∀x > 0, ∃n, ∀m ≥ n, abs (f n - f m) < x 56 57 def cau_seq : Type := 58 {f : N → Q // is_cau_seq f} 59 60 -- two sequences represent same real number when their difference converges to zero 61 @[instance] def cau_seq.setoid : setoid cau_seq := 62 { r := λf g : cau_seq, ∀x > 0, ∃n, ∀m ≥ n, abs (seq_of f m - seq_of g m) < x, 63 iseqv := by /- proof -/ } 64 65 def real : Type := quotient cau_seq.setoid 66 namespace real 67 68 @[instance] def has_zero : has_zero real := 69 { zero := ⟦cau_seq.const 0⟧ } 70 71 @[instance] def has_one : has_one real := 72 { one := ⟦cau_seq.const 1⟧ } 73 74 @[instance] def has_add : has_add real := 75 { add := quotient.lift₂ (λ a h : cau_seq, ⟦a + b ⟧) 76 by /- proof -/ } 77 end real 78 ``` 79