`universalInstantiationCert`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.UniversalInstantiationFromDistinction
domain: Foundation
line: 198 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.UniversalInstantiationFromDistinction on GitHub at line 198.

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

 195      ∃ x y : K, ∃ hxy : x ≠ y,
 196        Nonempty (LogicRealization.{u, 0})
 197
 198theorem universalInstantiationCert
 199    (K : Type u) [Nonempty K] :
 200    UniversalInstantiationCert K where
 201  instantiate := exists_logicRealization_of_distinction K
 202  named := exists_named_logicRealization_of_distinction K
 203
 204end UniversalInstantiationFromDistinction
 205end Foundation
 206end IndisputableMonolith

papers checked against this theorem

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