theorem proved term proof

`specifiabilityClosureCert`

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

formal statement (Lean)

  96theorem specifiabilityClosureCert (K : Type*) [Nonempty K] :
  97    SpecifiabilityClosureCert K where
  98  equivalence := distinguishability_iff_nontrivial_specifiability

proof body

Term-mode proof.

  99
 100end SpecifiabilityClosure
 101end Foundation
 102end IndisputableMonolith

depends on (4)

Lean names referenced from this declaration's body.

K in IndisputableMonolith.Constants decl_use
K in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
distinguishability_iff_nontrivial_specifiability in IndisputableMonolith.Foundation.DistinguishabilityFromSpecifiability decl_use
SpecifiabilityClosureCert in IndisputableMonolith.Foundation.DistinguishabilityFromSpecifiability decl_use