Icc_inter_Icc — Mathlib

English

For any a1 ≤ b1 and a2 ≤ b2 in a lattice, the intersection Icc(a1,b1) ∩ Icc(a2,b2) equals Icc(max(a1,a2), min(b1,b2)).

Русский

Пересечение двух замкнутых интервалов равно интервалу между максимумом нижних границ и минимумом верхних границ.

LaTeX

$$Icc a1 b1 ∩ Icc a2 b2 = Icc (a1 ⊔ a2) (b1 ⊓ b2)$$

Lean4

theorem Icc_inter_Icc : Icc a₁ b₁ ∩ Icc a₂ b₂ = Icc (a₁ ⊔ a₂) (b₁ ⊓ b₂) := by
  simp only [Ici_inter_Iic.symm, Ici_inter_Ici.symm, Iic_inter_Iic.symm]; ac_rfl

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