Iic_erase — Mathlib

English

Removing the endpoint b from the closed lower interval Iic(b) yields the open lower interval Iio(b): (Iic(b)) \ {b} = Iio(b).

Русский

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

LaTeX

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

Lean4

@[simp]
theorem Iic_erase [DecidableEq α] (b : α) : (Iic b).erase b = Iio b :=
  by
  ext
  simp_rw [Finset.mem_erase, mem_Iic, mem_Iio, lt_iff_le_and_ne, and_comm]

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