`toReal`

definition

show as: view math explainer →

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

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

  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
  97  · exact congrArg toReal
  98  · intro h
  99    have := congrArg fromReal h
 100    rw [fromReal_toReal, fromReal_toReal] at this
 101    exact this
 102

papers checked against this theorem

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