Ico_union_Ico' — Mathlib

English

The union of two half-open intervals equals a larger half-open interval given c ≤ b and a ≤ d: Ico a b ∪ Ico c d = Ico(min a c, max b d).

Русский

Объединение двух полупринятых интервалов равно большему полупринятому интервалу при условиях c ≤ b и a ≤ d.

LaTeX

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

Lean4

theorem Ico_union_Ico' {a b c d : α} (hcb : c ≤ b) (had : a ≤ d) : 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' hcb had]

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