natCast_add_of_omega0_le — Mathlib

English

Let o be an ordinal with ω ≤ o. Then for every natural number n, n + o = o.

Русский

Пусть o — ординал, удовлетворяющий ω ≤ o. Тогда для каждого натурального числа n выполняется n + o = o.

LaTeX

$$$\forall o\, (\omega \le o) \rightarrow \forall n \in \mathbb{N},\ n + o = o$$$

Lean4

@[simp]
theorem natCast_add_of_omega0_le {o} (h : ω ≤ o) (n : ℕ) : n + o = o := by
  rw [← Ordinal.add_sub_cancel_of_le h, ← add_assoc, natCast_add_omega0]

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