`bourbaki_complete`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.RealsFromLogic on GitHub at line 208.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 205
 206/-- The underlying Bourbaki completion is complete. This is the formal
 207completion theorem for the recovered real layer. -/
 208theorem bourbaki_complete : CompleteSpace CompareReals.Bourbakiℝ := by
 209  change CompleteSpace (Completion CompareReals.Q)
 210  infer_instance
 211
 212/-- Every recovered real is represented by a Mathlib real and vice versa. -/
 213theorem logicReal_recovered_from_completion :
 214    (∀ x : LogicReal, fromReal (toReal x) = x) ∧
 215    (∀ x : ℝ, toReal (fromReal x) = x) :=
 216  ⟨fromReal_toReal, toReal_fromReal⟩
 217
 218end LogicReal
 219
 220end
 221
 222end RealsFromLogic
 223end Foundation
 224end IndisputableMonolith

papers checked against this theorem

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