pith. machine review for the scientific record. sign in
theorem proved term proof

logicReal_recovered_from_completion

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 213theorem logicReal_recovered_from_completion :
 214    (∀ x : LogicReal, fromReal (toReal x) = x) ∧
 215    (∀ x : ℝ, toReal (fromReal x) = x) :=

proof body

Term-mode proof.

 216  ⟨fromReal_toReal, toReal_fromReal⟩
 217
 218end LogicReal
 219
 220end
 221
 222end RealsFromLogic
 223end Foundation
 224end IndisputableMonolith

depends on (6)

Lean names referenced from this declaration's body.