`categoricalMathlibCert_holds`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.UniversalForcing.Strict.CategoricalMathlib
domain: Foundation
line: 112 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.UniversalForcing.Strict.CategoricalMathlib on GitHub at line 112.

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

 109      g LogicNat.zero = base → (∀ n, g (LogicNat.succ n) = step (g n)) →
 110      f = g
 111
 112theorem categoricalMathlibCert_holds : CategoricalMathlibCert :=
 113{ recursor_zero_eq := @recursor_zero
 114  recursor_succ_eq := @recursor_succ
 115  universal_existence := @nno_universal_existence
 116  universal_uniqueness := @nno_universal_uniqueness }
 117
 118end
 119
 120end IndisputableMonolith.Foundation.UniversalForcing.Strict.CategoricalMathlib

papers checked against this theorem

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