Ico_pred_singleton

Mathlib.Order.Interval.Finset.Nat

URI: https://scilib.ai/kg/mathlib#Nat.Ico_pred_singleton

English

If a > 0, then Ico (a − 1) a is the singleton {a − 1}.

Русский

Если a > 0, то Ico (a − 1) a является синглтоном {a − 1}.

LaTeX

$$$ \text{Ico}(a-1, a) = \{a-1\} \quad\text{for } a>0, $$$

Lean4

@[simp]
theorem Ico_pred_singleton {a : ℕ} (h : 0 < a) : Ico (a - 1) a = {a - 1} := by rw [← Icc_pred_right _ h, Icc_self]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru