`admissibleClassCert_holds`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.UniversalForcing.AdmissibleClass
domain: Foundation
line: 131 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.UniversalForcing.AdmissibleClass on GitHub at line 131.

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

 128    ∀ R S : StrictLogicRealization,
 129      AdmissibleRealization R → AdmissibleRealization S → True
 130
 131noncomputable def admissibleClassCert_holds : AdmissibleClassCert :=
 132{ music_adm := music_admissible
 133  biology_adm := biology_admissible
 134  narrative_adm := narrative_admissible
 135  ethics_adm := ethics_admissible
 136  quantified_uf_holds := quantified_universal_forcing }
 137
 138end
 139
 140end IndisputableMonolith.Foundation.UniversalForcing.AdmissibleClass

papers checked against this theorem

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