veblenWith_lt_veblenWith_veblenWith_iff

English

If h: o2 ≤ o1, then veblenWith(f,o2,a) < veblenWith(f,o1,veblenWith(f,o2,a)) iff a < veblenWith(f,o1,a).

Русский

Пусть o2 ≤ o1. Тогда veblenWith(f,o2,a) < veblenWith(f,o1,veblenWith(f,o2,a)) эквивалентно a < veblenWith(f,o1,a).

LaTeX

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

Lean4

theorem veblenWith_lt_veblenWith_veblenWith_iff (h : o₂ ≤ o₁) :
    veblenWith f o₂ a < veblenWith f o₁ (veblenWith f o₂ a) ↔ a < veblenWith f o₁ a := by
  simp_rw [(right_le_veblenWith hf ..).lt_iff_ne', ne_eq, veblenWith_veblenWith_eq_veblenWith_iff hf h]

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