isNormal_add_right — Mathlib

English

For every ordinal a, the map x ↦ a + x is normal (strictly increasing and continuous from below).

Русский

Для каждого ординала a отображение x ↦ a + x является нормальным (строго возрастает и сохраняет пределы снизу).

LaTeX

$$∀ a, IsNormal (a + ·)$$

Lean4

theorem isNormal_add_right (a : Ordinal) : IsNormal (a + ·) :=
  by
  rw [isNormal_iff_strictMono_limit]
  exact ⟨add_right_strictMono, fun _ l _ ↦ (add_le_iff_of_isSuccLimit l).2⟩

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