veblenWith_zero_inj — Mathlib

English

If 0 < f(0), then veblenWith(f, o1, 0) = veblenWith(f, o2, 0) iff o1 = o2.

Русский

Если 0 < f(0), тогда veblenWith(f, o1, 0) = veblenWith(f, o2, 0) эквивалентно o1 = o2.

LaTeX

$$$\forall f:\,\operatorname{Ordinal} \to \operatorname{Ordinal},\ \operatorname{IsNormal}(f) \Rightarrow (0 < f(0)) \Rightarrow (\operatorname{veblenWith}(f,o1,0) = \operatorname{veblenWith}(f,o2,0) \iff o1 = o2)$$$

Lean4

theorem veblenWith_zero_inj (hp : 0 < f 0) : veblenWith f o₁ 0 = veblenWith f o₂ 0 ↔ o₁ = o₂ :=
  (veblenWith_zero_strictMono hf hp).injective.eq_iff

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