veblenWith_le_veblenWith_iff — Mathlib

English

For hp: 0 < f(0) we have veblenWith(f,o1,a) ≤ veblenWith(f,o2,b) iff o1 = o2 and a ≤ b, or o1 < o2 and a ≤ veblenWith(f,o2,b), or o2 < o1 and veblenWith(f,o1,a) ≤ b.

Русский

При hp: 0 < f(0) выполняется неубывание: veblenWith(f,o1,a) ≤ veblenWith(f,o2,b) эквивалентно одному из трёх случаев: o1=o2 и a≤b, или o1<o2 и a≤veblenWith(f,o2,b), или o2<o1 и veblenWith(f,o1,a)≤b.

LaTeX

$$$\forall f:\,\operatorname{Ordinal} \to \operatorname{Ordinal},\ \operatorname{IsNormal}(f)\Rightarrow \forall o1,o2,a,b:\operatorname{Ordinal},\ hp:\, 0 < f(0)\Rightarrow \ \operatorname{veblenWith}(f,o1,a) \le \operatorname{veblenWith}(f,o2,b) \iff \operatorname{(o1=o2 \land a\le b) \lor (o1

Lean4

/-- `veblenWith f o₁ a ≤ veblenWith f o₂ b` iff one of the following holds:
* `o₁ = o₂` and `a ≤ b`
* `o₁ < o₂` and `a ≤ veblenWith f o₂ b`
* `o₁ > o₂` and `veblenWith f o₁ a ≤ b` -/
theorem veblenWith_le_veblenWith_iff :
    veblenWith f o₁ a ≤ veblenWith f o₂ b ↔
      o₁ = o₂ ∧ a ≤ b ∨ o₁ < o₂ ∧ a ≤ veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a ≤ b :=
  by
  rw [← not_lt, ← cmp_eq_gt_iff, cmp_veblenWith hf]
  aesop (add simp [not_lt_of_ge, lt_asymm])

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