Ico_union_Ico — Mathlib

English

If a ≤ b and b ≤ c, then Ico(a,b) ∪ Ico(b,c) = Ico(a,c).

Русский

Если a ≤ b и b ≤ c, то Ico(a,b) ∪ Ico(b,c) = Ico(a,c).

LaTeX

$$$ (a \le b) \land (b \le c) \implies Ico(a,b) \cup Ico(b,c) = Ico(a,c). $$$

Lean4

theorem Ico_union_Ico (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
  rcases le_total a b with hab | hab <;> rcases le_total c d with hcd | hcd <;> simp [*] at h₁ h₂
  · exact Ico_union_Ico' h₂ h₁
  all_goals simp [*]

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