equivReal

formal source

  84  simp [toReal, fromReal]
  85
  86/-- Carrier equivalence between recovered reals and Mathlib reals. -/
  87noncomputable def equivReal : LogicReal ≃ ℝ where
  88  toFun := toReal
  89  invFun := fromReal
  90  left_inv := fromReal_toReal
  91  right_inv := toReal_fromReal
  92
  93/-- Equality transfer: recovered real equality is exactly equality after
  94transport to Mathlib's real line. -/
  95theorem eq_iff_toReal_eq {x y : LogicReal} : x = y ↔ toReal x = toReal y := by
  96  constructor
  97  · exact congrArg toReal
  98  · intro h
  99    have := congrArg fromReal h
 100    rw [fromReal_toReal, fromReal_toReal] at this
 101    exact this
 102
 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