ofRatCore

formal source

 103/-! ## 3. Embedding of recovered rationals -/
 104
 105/-- Coerce a Mathlib rational into the Bourbaki completion. -/
 106noncomputable def ofRatCore (q : ℚ) : LogicReal :=
 107  ⟨Completion.coe' (show CompareReals.Q from q)⟩
 108
 109/-- Embed a recovered rational into `LogicReal`. -/
 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