`LogicReal`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.RealsFromLogic
domain: Foundation
line: 66 · 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 66.

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

used by

formal source

  63
  64The wrapper prevents global instance pollution on `Completion ℚ` while still
  65letting us reuse Mathlib's completed real line. -/
  66structure LogicReal where
  67  val : CompareReals.Bourbakiℝ
  68
  69namespace LogicReal
  70
  71/-- Transport a recovered real to Mathlib's real line. -/
  72noncomputable def toReal (x : LogicReal) : ℝ :=
  73  CompareReals.compareEquiv x.val
  74
  75/-- Transport a Mathlib real into the recovered real line. -/
  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

papers checked against this theorem

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