Ioc_diff_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem Ioc_diff_right : Ioc a b \ { b } = Ioo a b :=
  ext fun x => by simp [and_assoc, ← lt_iff_le_and_ne]

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