toReal_ofRatCore

formal source

 110noncomputable def ofLogicRat (q : LogicRat) : LogicReal :=
 111  ofRatCore (toRat q)
 112
 113theorem toReal_ofRatCore (q : ℚ) : toReal (ofRatCore q) = (q : ℝ) := by
 114  -- `CompareReals.compareEquiv` is the unique completion comparison map;
 115  -- on dense rational points it agrees with the usual rational coercion.
 116  simpa [toReal, ofRatCore, CompareReals.compareEquiv] using
 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 _