Ioc_union_Ioc_union_Ioc_cycle — Mathlib

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]

Похожие утверждения