English
If min a b < max c d and min c d < max a b, then Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d).
Русский
Если min(a,b) < max(c,d) и min(c,d) < max(a,b), то Ioo(a,b) ∪ Ioo(c,d) = Ioo(min(a,c), max(b,d)).
LaTeX
$$$(\min(a,b) < \max(c,d)) \land (\min(c,d) < \max(a,b)) \implies \mathrm{Ioo}(a,b) \cup \mathrm{Ioo}(c,d) = \mathrm{Ioo}(\min(a,c), \max(b,d))$$$
Lean4
theorem Ioo_union_Ioo (h₁ : min a b < max c d) (h₂ : min c d < max a b) : Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d) :=
by
rcases le_total a b with hab | hab <;> rcases le_total c d with hcd | hcd <;>
simp only [min_eq_left, min_eq_right, max_eq_left, max_eq_right, hab, hcd] at h₁ h₂
· exact Ioo_union_Ioo' h₂ h₁
all_goals simp [*, le_of_lt h₂, le_of_lt h₁]
