logicNat_NNO_uniqueness

formal source

  24        ∀ n, f (LogicNat.succ n) = step (f n) :=
  25  @nno_universal_existence
  26
  27theorem logicNat_NNO_uniqueness :
  28    ∀ {α : Type*} (base : α) (step : α → α)
  29      (f g : LogicNat → α),
  30      f LogicNat.zero = base → (∀ n, f (LogicNat.succ n) = step (f n)) →
  31      g LogicNat.zero = base → (∀ n, g (LogicNat.succ n) = step (g n)) →
  32      f = g :=
  33  @nno_universal_uniqueness
  34
  35structure MathlibNNOCert where
  36  exists_rec :
  37    ∀ {α : Type*} (base : α) (step : α → α),
  38      ∃ (f : LogicNat → α),
  39        f LogicNat.zero = base ∧
  40        ∀ n, f (LogicNat.succ n) = step (f n)
  41  unique_rec :
  42    ∀ {α : Type*} (base : α) (step : α → α)
  43      (f g : LogicNat → α),
  44      f LogicNat.zero = base → (∀ n, f (LogicNat.succ n) = step (f n)) →
  45      g LogicNat.zero = base → (∀ n, g (LogicNat.succ n) = step (g n)) →
  46      f = g
  47
  48theorem mathlibNNOCert_holds : MathlibNNOCert :=
  49{ exists_rec := logicNat_has_type_NNO_universal_property
  50  unique_rec := logicNat_NNO_uniqueness }
  51
  52end
  53
  54end IndisputableMonolith.Foundation.UniversalForcing.Strict.MathlibNNO