Ico_diff_Ioo_self — Mathlib

English

If a < b, then the half-open interval Ico(a,b) minus the open interval Ioo(a,b) is exactly the singleton {a}.

Русский

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

LaTeX

$$$$ a < b \Rightarrow Ico(a,b) \setminus Ioo(a,b) = \{a\} $$$$

Lean4

@[simp]
theorem Ico_diff_Ioo_self (h : a < b) : Ico a b \ Ioo a b = { a } := by simp [← coe_inj, h]

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