Icc_union_Ici — Mathlib

English

If c ≤ max(a,b), then [a,b] ∪ [c, ∞) = [min(a,c), ∞).

Русский

Если c ≤ max(a,b), то [a,b] ∪ [c, ∞) = [min(a,c), ∞).

LaTeX

$$$[a,b] \cup [c,\infty) = [\min(a,c), \infty) \quad (c \le \max(a,b)).$$

Lean4

theorem Icc_union_Ici (h : c ≤ max a b) : Icc a b ∪ Ici c = Ici (min a c) :=
  by
  rcases le_or_gt a b with hab | hab
  · simp only [hab, sup_of_le_right] at h; exact Icc_union_Ici' h
  · simp only [le_sup_iff] at h; rcases h with h | h
    · simp [*]
    · have hca : c ≤ a := h.trans hab.le
      simp [*]

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