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