English
Let α be a linearly ordered set and b,c,d ∈ α with min{c,d} < b. Then [−∞, b] ∪ (c, d] = [−∞, max{b,d}].
Русский
Пусть α — линейно упорядоченное множество, и b, c, d ∈ α удовлетворяют min{c,d} < b. Тогда {x : x ≤ b} ∪ {x : c < x ≤ d} = {x : x ≤ max(b,d)}.
LaTeX
$$$ \min(c,d) < b \implies Iic(b) \cup Ioc(c,d) = Iic(\max(b,d)). $$$
Lean4
theorem Iic_union_Ioc (h : min c d < b) : Iic b ∪ Ioc c d = Iic (max b d) :=
by
rcases le_total c d with hcd | hcd
· simp only [hcd, inf_of_le_left] at h; exact Iic_union_Ioc' h
· rw [max_comm]
simp_all [max_eq_right_of_lt]