`fromReal_toReal`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.RealsFromLogic
domain: Foundation
line: 82 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.RealsFromLogic on GitHub at line 82.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  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`. -/
 110noncomputable def ofLogicRat (q : LogicRat) : LogicReal :=
 111  ofRatCore (toRat q)
 112

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.