structure
definition
def or abbrev
CategoricalMathlibCert
show as:
view Lean formalization →
formal statement (Lean)
98structure CategoricalMathlibCert where
99 recursor_zero_eq : ∀ {α : Type*} (base : α) (step : α → α),
100 recursor base step LogicNat.zero = base
101 recursor_succ_eq : ∀ {α : Type*} (base : α) (step : α → α) (n : LogicNat),
102 recursor base step (LogicNat.succ n) = step (recursor base step n)
103 universal_existence : ∀ {α : Type*} (base : α) (step : α → α),
104 ∃ (f : LogicNat → α),
105 f LogicNat.zero = base ∧ ∀ n, f (LogicNat.succ n) = step (f n)
106 universal_uniqueness : ∀ {α : Type*} (base : α) (step : α → α)
107 (f g : LogicNat → α),
108 f LogicNat.zero = base → (∀ n, f (LogicNat.succ n) = step (f n)) →
109 g LogicNat.zero = base → (∀ n, g (LogicNat.succ n) = step (g n)) →
110 f = g
111