`LogicReal`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.RealsFromLogic on GitHub at line 66.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

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.