Ico_zero_eq_range — Mathlib

English

For every natural number n, the half-open interval Ico(0,n) coincides with the initial segment range(n).

Русский

Для каждого натурального числа n полузакрытый интервал Ico(0,n) совпадает с диапазоном range(n).

LaTeX

$$$\forall n \in \mathbb{N},\ Ico(0,n) = \operatorname{range}(n)$$$

Lean4

@[simp]
theorem Ico_zero_eq_range : Ico 0 = range := by rw [← Nat.bot_eq_zero, ← Iio_eq_Ico, Iio_eq_range]

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