theorem proved term proof

`mathlibNNOCert_holds`

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

formal statement (Lean)

  48theorem mathlibNNOCert_holds : MathlibNNOCert :=

proof body

Term-mode proof.

  49{ exists_rec := logicNat_has_type_NNO_universal_property
  50  unique_rec := logicNat_NNO_uniqueness }
  51
  52end
  53
  54end IndisputableMonolith.Foundation.UniversalForcing.Strict.MathlibNNO

depends on (3)

Lean names referenced from this declaration's body.

logicNat_has_type_NNO_universal_property in IndisputableMonolith.Foundation.UniversalForcing.Strict.MathlibNNO decl_use
logicNat_NNO_uniqueness in IndisputableMonolith.Foundation.UniversalForcing.Strict.MathlibNNO decl_use
MathlibNNOCert in IndisputableMonolith.Foundation.UniversalForcing.Strict.MathlibNNO decl_use