Ico_eq_cons_Ioo — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- `Finset.cons` version of `Finset.Ioo_insert_left`. -/
theorem Ico_eq_cons_Ioo (h : a < b) : Ico a b = (Ioo a b).cons a left_notMem_Ioo := by
  classical rw [cons_eq_insert, Ioo_insert_left h]

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