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]