structure definition def or abbrev

`NontrivialSpecification`

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

formal statement (Lean)

  21structure NontrivialSpecification (K : Type*) where
  22  inOntology : K → Prop
  23  someInside : ∃ x : K, inOntology x
  24  someOutside : ∃ x : K, ¬ inOntology x
  25
  26/-- Specifiability forces distinguishability. -/

used by (8)

From the project-wide theorem graph. These declarations reference this one in their body.

AbsoluteFloorClosureCert in IndisputableMonolith.Foundation.AbsoluteFloorClosure decl_use
AbsoluteFloorWitness in IndisputableMonolith.Foundation.AbsoluteFloorClosure decl_use
at_most_one_of_no_nontrivial_specification in IndisputableMonolith.Foundation.DistinguishabilityFromSpecifiability decl_use
distinguishability_from_specification in IndisputableMonolith.Foundation.DistinguishabilityFromSpecifiability decl_use
distinguishability_iff_nontrivial_specifiability in IndisputableMonolith.Foundation.DistinguishabilityFromSpecifiability decl_use
nontrivial_spec_from_proper_ontology in IndisputableMonolith.Foundation.DistinguishabilityFromSpecifiability decl_use
nontrivial_specification_of_proper_subtype in IndisputableMonolith.Foundation.DistinguishabilityFromSpecifiability decl_use
SpecifiabilityClosureCert in IndisputableMonolith.Foundation.DistinguishabilityFromSpecifiability decl_use

depends on (3)

Lean names referenced from this declaration's body.

K in IndisputableMonolith.Constants decl_use
K in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
forces in IndisputableMonolith.Foundation.MagnitudeOfMismatch decl_use