veblenWith_veblenWith_eq_veblenWith_iff

English

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

Русский

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

LaTeX

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

Lean4

theorem veblenWith_veblenWith_eq_veblenWith_iff (h : o₂ ≤ o₁) :
    veblenWith f o₁ (veblenWith f o₂ a) = veblenWith f o₂ a ↔ veblenWith f o₁ a = a := by
  grind [veblenWith_inj, → veblenWith_eq_self_of_le]

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