Ioc_eq_cons_Ioo — Mathlib

English

If a < b, the half-open interval Ioc(a,b) is Ioo(a,b) with the right endpoint b adjoined; i.e., Ioc(a,b) = Ioo(a,b) ∪ {b}.

Русский

Если a < b, то Ioc(a,b) состоит из Ioo(a,b) и правого конца b: Ioc(a,b) = Ioo(a,b) ∪ {b}.

LaTeX

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

Lean4

/-- `Finset.cons` version of `Finset.Ioo_insert_right`. -/
theorem Ioc_eq_cons_Ioo (h : a < b) : Ioc a b = (Ioo a b).cons b right_notMem_Ioo := by
  classical rw [cons_eq_insert, Ioo_insert_right h]

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