apply_lt_veblenWith_apply_iff — Mathlib

English

For any f normal, the statement f(a) < veblenWith(f, o, f(a)) is equivalent to a < veblenWith(f, o, a).

Русский

Для любого нормального f: f(a) < veblenWith(f, o, f(a)) эквивалентно a < veblenWith(f, o, a).

LaTeX

$$$\forall f:\,\operatorname{Ordinal} \to \operatorname{Ordinal},\ \operatorname{IsNormal}(f)\Rightarrow \left( f(a) < \operatorname{veblenWith}(f,o,(f\,a)) \iff a < \operatorname{veblenWith}(f,o,a) \right)$$$

Lean4

theorem apply_lt_veblenWith_apply_iff : f a < veblenWith f o (f a) ↔ a < veblenWith f o a := by
  simpa using veblenWith_lt_veblenWith_veblenWith_iff hf (zero_le o)

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