Iic_union_Icc — Mathlib

English

In a linear order, for appropriate c ≤ b, the union 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 : min c d ≤ b) : Iic b ∪ Icc c d = Iic (max b d) :=
  by
  rcases le_or_gt c d with hcd | hcd
  · simp only [hcd, inf_of_le_left] at h; exact Iic_union_Icc' h
  · simp only [inf_le_iff] at h; rcases h with h | h
    · have hdb : d ≤ b := hcd.le.trans h
      simp [*]
    · simp [*]

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