def
definition
self_reference_complete
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.RRF.Foundation.SelfReference on GitHub at line 206.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
is -
is -
is -
is -
rrf_internally_consistent -
rrf_is_fixed_point -
SelfReferenceComplete -
thisFile -
this_is_recognition
used by
formal source
203 compilation_is_recognition : CompilationAsRecognition
204
205/-- The self-reference structure is complete. -/
206def self_reference_complete : SelfReferenceComplete := {
207 meta_rrf := thisFile,
208 is_fixed_point := rrf_is_fixed_point,
209 is_consistent := rrf_internally_consistent,
210 compilation_is_recognition := this_is_recognition
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