English
Let α be a linearly ordered set and a, b, c ∈ α with b between a and c in the unordered sense. Then uIoc(a, b) ∪ uIoc(b, c) = uIoc(a, c).
Русский
Пусть α — линейно упорядоченное множество, и пусть a, b, c ∈ α удовлетворяют условию, что b лежит между a и c в неупорядоченном смысле. Тогда uIoc(a, b) ∪ uIoc(b, c) = uIoc(a, c).
LaTeX
$$$ \min(a,c) \le b \le \max(a,c) \implies uIoc(a,b) \cup uIoc(b,c) = uIoc(a,c) $$$
Lean4
theorem uIoc_union_uIoc (h : b ∈ [[a, c]]) : Ι a b ∪ Ι b c = Ι a c :=
by
wlog hac : a ≤ c generalizing a c
· rw [uIoc_comm, union_comm, uIoc_comm, this _ (le_of_not_ge hac), uIoc_comm]
rwa [uIcc_comm]
rw [uIcc_of_le hac] at h
rw [uIoc_of_le h.1, uIoc_of_le h.2, uIoc_of_le hac, Ioc_union_Ioc_eq_Ioc h.1 h.2]
