Icc_eq_cons_Ioc — Mathlib

English

If a ≤ b, the closed interval Icc(a,b) is Ioc(a,b) plus the left endpoint a; i.e., Icc(a,b) = Ioc(a,b) ∪ {a}.

Русский

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

LaTeX

$$$$ a \le b \Rightarrow Icc(a,b) = Ioc(a,b) \cup \{a\} $$$$

Lean4

/-- `Finset.cons` version of `Finset.Ioc_insert_left`. -/
theorem Icc_eq_cons_Ioc (h : a ≤ b) : Icc a b = (Ioc a b).cons a left_notMem_Ioc := by
  classical rw [cons_eq_insert, Ioc_insert_left h]

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