toReal_ofLogicRat

formal source

 117    (CompareReals.bourbakiPkg.compare_coe rationalCauSeqPkg
 118      (show CompareReals.Q from q))
 119
 120theorem toReal_ofLogicRat (q : LogicRat) : toReal (ofLogicRat q) = (toRat q : ℝ) := by
 121  rw [ofLogicRat, toReal_ofRatCore]
 122
 123/-! ## 4. Algebra and order by transport through `toReal` -/
 124
 125instance : Zero LogicReal := ⟨fromReal 0⟩
 126instance : One LogicReal := ⟨fromReal 1⟩
 127instance : Add LogicReal := ⟨fun x y => fromReal (toReal x + toReal y)⟩
 128instance : Neg LogicReal := ⟨fun x => fromReal (-toReal x)⟩
 129instance : Sub LogicReal := ⟨fun x y => fromReal (toReal x - toReal y)⟩
 130instance : Mul LogicReal := ⟨fun x y => fromReal (toReal x * toReal y)⟩
 131instance : Inv LogicReal := ⟨fun x => fromReal (toReal x)⁻¹⟩
 132instance : Div LogicReal := ⟨fun x y => fromReal (toReal x / toReal y)⟩
 133instance : LE LogicReal := ⟨fun x y => toReal x ≤ toReal y⟩
 134instance : LT LogicReal := ⟨fun x y => toReal x < toReal y⟩
 135
 136@[simp] theorem toReal_zero : toReal (0 : LogicReal) = 0 := toReal_fromReal 0
 137@[simp] theorem toReal_one : toReal (1 : LogicReal) = 1 := toReal_fromReal 1
 138@[simp] theorem toReal_add (x y : LogicReal) : toReal (x + y) = toReal x + toReal y :=
 139  toReal_fromReal _
 140@[simp] theorem toReal_neg (x : LogicReal) : toReal (-x) = -toReal x :=
 141  toReal_fromReal _
 142@[simp] theorem toReal_sub (x y : LogicReal) : toReal (x - y) = toReal x - toReal y :=
 143  toReal_fromReal _
 144@[simp] theorem toReal_mul (x y : LogicReal) : toReal (x * y) = toReal x * toReal y :=
 145  toReal_fromReal _
 146@[simp] theorem toReal_inv (x : LogicReal) : toReal x⁻¹ = (toReal x)⁻¹ :=
 147  toReal_fromReal _
 148@[simp] theorem toReal_div (x y : LogicReal) : toReal (x / y) = toReal x / toReal y :=
 149  toReal_fromReal _
 150