Iio_insert — Mathlib

English

Inserting the endpoint b into the open lower interval Iio(b) yields the closed lower interval Iic(b): Iio(b) ∪ {b} = Iic(b).

Русский

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

LaTeX

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

Lean4

@[simp]
theorem Iio_insert [DecidableEq α] (b : α) : insert b (Iio b) = Iic b :=
  by
  ext
  simp_rw [Finset.mem_insert, mem_Iic, mem_Iio, le_iff_lt_or_eq, or_comm]

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