toReal_fromReal

formal source

  76noncomputable def fromReal (x : ℝ) : LogicReal :=
  77  ⟨CompareReals.compareEquiv.symm x⟩
  78
  79theorem toReal_fromReal (x : ℝ) : toReal (fromReal x) = x := by
  80  simp [toReal, fromReal]
  81
  82theorem fromReal_toReal (x : LogicReal) : fromReal (toReal x) = x := by
  83  cases x
  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`. -/