theorem
proved
self_reference_witnessed
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.RRF.Foundation.SelfReference on GitHub at line 214.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
211}
212
213/-- Self-reference completeness is witnessed. -/
214theorem self_reference_witnessed : Nonempty SelfReferenceComplete :=
215 ⟨self_reference_complete⟩
216
217end RRF.Foundation.SelfReference
218end IndisputableMonolith