iSup_mul_nat — Mathlib

English

For any ordinal o, the supremum over natural numbers of o * n equals o * ω.

Русский

Для ординала o супремум по n∈ℕ от o*n равен o*ω.

LaTeX

$$$\\forall o\\; (\\sup_{n\\in\\mathbb{N}} o \\cdot n) = o \\cdot \\omega$$$

Lean4

@[simp]
theorem iSup_mul_nat (o : Ordinal) : ⨆ n : ℕ, o * n = o * ω :=
  by
  rcases eq_zero_or_pos o with (rfl | ho)
  · rw [zero_mul]
    exact iSup_eq_zero_iff.2 fun n => zero_mul (n : Ordinal)
  · exact (isNormal_mul_right ho).apply_omega0

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