72structure PeanoSurface {R : LogicRealization} (A : ArithmeticOf R) : Prop where 73 zero_ne_step : ∀ x : A.peano.carrier, A.peano.zero ≠ A.peano.step x 74 step_injective : Function.Injective A.peano.step 75 induction : 76 ∀ P : A.peano.carrier → Prop, 77 P A.peano.zero → 78 (∀ n, P n → P (A.peano.step n)) → 79 ∀ n, P n 80 81/-! ## LogicNat as the canonical initial Peano object -/ 82 83/-- The Peano object carried by `LogicNat`. -/
used by (7)
From the project-wide theorem graph. These declarations reference this one in their body.