Ici_eq_cons_Ioi — Mathlib

English

The closed upper interval [a, ∞) is obtained by adding a to the open upper interval (a, ∞); equivalently, Ici(a) = {a} ∪ Ioi(a).

Русский

Закрытый верхний интервал [a, ∞) получаем добавлением a к открытому верхнему интервалу (a, ∞); то есть Ici(a) = {a} ∪ Ioi(a).

LaTeX

$$$ Ici(a) = \{a\} \cup Ioi(a) $$$

Lean4

/-- `Finset.cons` version of `Finset.Ioi_insert`. -/
theorem Ici_eq_cons_Ioi (a : α) : Ici a = (Ioi a).cons a notMem_Ioi_self := by classical rw [cons_eq_insert, Ioi_insert]

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