isNormal_mul_right — Mathlib

English

If a > 0, then the map x ↦ a · x is a normal function on ordinals (i.e., preserves certain order-theoretic limits).

Русский

Если a > 0, то отображение x ↦ a · x является нормальной функцией на ординалах (сохраняет пределы по порядку).

LaTeX

$$$\forall a \in \mathrm{Ordinal},\ a > 0\Rightarrow \mathrm{IsNormal}(\lambda x.~ a \cdot x)$$$

Lean4

theorem isNormal_mul_right {a : Ordinal} (h : 0 < a) : IsNormal (a * ·) :=
  by
  refine IsNormal.of_succ_lt (fun b ↦ ?_) fun hb ↦ ?_
  · simpa [mul_succ] using (add_lt_add_iff_left (a * b)).2 h
  ·
    simpa [IsLUB, IsLeast, upperBounds, lowerBounds, mul_le_iff_of_isSuccLimit hb] using fun c hc ↦
      mul_le_mul_left' hc.le a

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