English
If certain semilattice and order conditions hold, the union of two Ico intervals equals Ico with min/max endpoints as given.
Русский
При выполнении условий полугруппы и порядка объединение двух интервалов Ico равно интервалу Ico со словами, минимизирующими начала и максимизирующими концы.
LaTeX
$$$ Ico(a,b) \cup Ico(c,d) = Ico(\min(a,c), \max(b,d)) $$$
Lean4
theorem Ico_union_Ico {a b c d : α} (h₁ : min a b ≤ max c d) (h₂ : min c d ≤ max a b) :
Ico a b ∪ Ico c d = Ico (min a c) (max b d) := by
rw [← coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, Set.Ico_union_Ico h₁ h₂]