module
module
IndisputableMonolith.Foundation.DistinguishabilityFromSpecifiability
show as:
view Lean formalization →
used by (1)
declarations in this module (8)
-
structure
NontrivialSpecification -
theorem
distinguishability_from_specification -
def
nontrivial_specification_of_proper_subtype -
def
nontrivial_spec_from_proper_ontology -
theorem
at_most_one_of_no_nontrivial_specification -
theorem
distinguishability_iff_nontrivial_specifiability -
structure
SpecifiabilityClosureCert -
theorem
specifiabilityClosureCert