Ico_union_Ico — Mathlib

English

If certain semilattice and order conditions hold, the union of two Ico intervals equals Ico with min/max endpoints as given.

Русский

При выполнении условий полугруппы и порядка объединение двух интервалов Ico равно интервалу Ico со словами, минимизирующими начала и максимизирующими концы.

LaTeX

$$$ Ico(a,b) \cup Ico(c,d) = Ico(\min(a,c), \max(b,d)) $$$

Lean4

theorem Ico_union_Ico {a b c d : α} (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
  rw [← coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, Set.Ico_union_Ico h₁ h₂]

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