English
The union Ioc a b ∪ Ioc b c ∪ Ioc c a equals Ioc (min a (min b c)) (max a (max b c)).
Русский
Объединение Ioc(a,b) ∪ Ioc(b,c) ∪ Ioc(c,a) равно Ioc(min(a, min(b,c)), max(a, max(b,c))).
LaTeX
$$$Ioc a b \\\\cup Ioc b c \\\\cup Ioc c a = Ioc (\\\\min a (\\\\min b c)) (\\\\max a (\\\\max b c))$$$
Lean4
@[simp]
theorem Ioc_union_Ioc_union_Ioc_cycle : Ioc a b ∪ Ioc b c ∪ Ioc c a = Ioc (min a (min b c)) (max a (max b c)) :=
by
rw [Ioc_union_Ioc, Ioc_union_Ioc]
· ac_rfl
all_goals
solve_by_elim (maxDepth := 5) [min_le_of_left_le, min_le_of_right_le, le_max_of_le_left, le_max_of_le_right,
le_refl]