Iic_union_Icc' — Mathlib

English

For c ≤ b in a linear order, Iic b ∪ Icc c d equals Iic (max b d).

Русский

Для c ≤ b в линейном порядке Iic b ∪ Icc c d равно Iic (max b d).

LaTeX

$$$ c \le b \implies Iic\, b \cup Icc\, c\, d = Iic\, (\max\, b\, d) $$$

Lean4

theorem Iic_union_Icc' (h₁ : c ≤ b) : Iic b ∪ Icc c d = Iic (max b d) :=
  by
  ext1 x
  simp_rw [mem_union, mem_Iic, mem_Icc, le_max_iff]
  by_cases hc : c ≤ x
  · tauto
  · have hxb : x ≤ b := (le_of_not_ge hc).trans h₁
    tauto

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