Icc_diff_left — Mathlib

English

Removing the left endpoint from a closed interval yields the open-closed interval on the right: Icc(a, b) \\ {a} = Ioc(a, b).

Русский

Удаление левой границы из замкнутого интервала даёт открыто-замкнутый интервал справа: Icc(a, b) \\ {a} = Ioc(a, b).

LaTeX

$$$$ Icc(a,b) \\ \\{a\\} = Ioc(a,b) $$$$

Lean4

@[simp]
theorem Icc_diff_left : Icc a b \ { a } = Ioc a b :=
  ext fun x => by simp [lt_iff_le_and_ne, eq_comm, and_right_comm]

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