Iic_eq_cons_Iio — Mathlib

English

The closed lower interval Iic(b) equals adding b to the open lower interval Iio(b): Iic(b) = {b} ∪ Iio(b).

Русский

Закрытый нижний интервал Iic(b) равен добавлению b к открытому нижнему интервалу Iio(b): Iic(b) = {b} ∪ Iio(b).

LaTeX

$$$ Iic(b) = \{b\} \cup Iio(b) $$$

Lean4

/-- `Finset.cons` version of `Finset.Iio_insert`. -/
theorem Iic_eq_cons_Iio (b : α) : Iic b = (Iio b).cons b notMem_Iio_self := by classical rw [cons_eq_insert, Iio_insert]

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