Ico_diff_Ioo_same — Mathlib

English

If a < b, then removing the open interval Ioo(a, b) from the half-open interval Ico(a, b) leaves exactly {a}: Ico(a,b) \\ Ioo(a,b) = {a}.

Русский

Если a < b, то из полузакрытого интервала Ico(a,b) удаление открытого интервала Ioo(a,b) оставляет ровно {a}.

LaTeX

$$$$ \\text{If } a < b: \\ Ico(a,b) \\ Ioo(a,b) = \\{a\\}. $$$$

Lean4

@[simp]
theorem Ico_diff_Ioo_same (h : a < b) : Ico a b \ Ioo a b = { a } := by
  rw [← Ico_diff_left, diff_diff_cancel_left (singleton_subset_iff.2 <| left_mem_Ico.2 h)]

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