eq_iff_zero_and_succ — Mathlib

English

Let f,g: Ordinal → Ordinal be normal functions. Then f = g if and only if f(0) = g(0) and for every a, f(a) = g(a) implies f(succ(a)) = g(succ(a)).

Русский

Пусть f, g: Ordinal → Ordinal — нормальные функции. Тогда f = g тогда и только тогда, когда f(0) = g(0) и для каждого a выполняется: f(a) = g(a) → f(succ(a)) = g(succ(a)).

LaTeX

$$$f = g \\iff f 0 = g 0 \\land \\forall a,\\ f a = g a \\rightarrow f(\\operatorname{succ} a) = g(\\operatorname{succ} a)$$$

Lean4

theorem eq_iff_zero_and_succ {f g : Ordinal.{u} → Ordinal.{u}} (hf : IsNormal f) (hg : IsNormal g) :
    f = g ↔ f 0 = g 0 ∧ ∀ a, f a = g a → f (succ a) = g (succ a) :=
  Order.IsNormal.ext hf hg

Похожие утверждения