Icc_eq_cons_Ico — Mathlib

English

If a ≤ b, the closed interval Icc(a,b) is obtained from Ico(a,b) by adjoining the endpoint b, i.e., Icc(a,b) = Ico(a,b) ∪ {b}.

Русский

Если a ≤ b, то закрытый интервал Icc(a,b) получается из Ico(a,b) добавлением конца b, т.е. Icc(a,b) = Ico(a,b) ∪ {b}.

LaTeX

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

Lean4

/-- `Finset.cons` version of `Finset.Ico_insert_right`. -/
theorem Icc_eq_cons_Ico (h : a ≤ b) : Icc a b = (Ico a b).cons b right_notMem_Ico := by
  classical rw [cons_eq_insert, Ico_insert_right h]

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