English
Equivalent form of Icc union Icc with h1/h2, expressing min/max endpoints.
Русский
Равносильная форма объединения интервальных множеств Icc с параметрами h1/h2, через минимальные и максимальные концы.
LaTeX
$$$\text{(same structural statement as Icc Union')}$$$
Lean4
/-- We cannot replace `<` by `≤` in the hypotheses.
Otherwise for `b < a = d < c` the l.h.s. is `∅` and the r.h.s. is `{a}`.
-/
theorem Icc_union_Icc (h₁ : min a b < max c d) (h₂ : min c d < max a b) : Icc a b ∪ Icc c d = Icc (min a c) (max b d) :=
by
rcases le_or_gt a b with hab | hab <;> rcases le_or_gt c d with hcd | hcd <;>
simp only [min_eq_left, max_eq_right, min_eq_right_of_lt, max_eq_left_of_lt, hab, hcd] at h₁ h₂
· exact Icc_union_Icc' h₂.le h₁.le
all_goals simp [*, min_eq_left_of_lt, max_eq_left_of_lt, min_eq_right_of_lt, max_eq_right_of_lt]
