Icc_prod_Icc — Mathlib

English

In a product lattice, the product of closed intervals is a closed interval: Icc a1 a2 ×ˢ Icc b1 b2 = Icc (a1,b1) (a2,b2).

Русский

В произведении решёток произведение двух замкнутых интервалов образует замкнутый интервал в паре: Icc(a1,b1) × Icc(a2,b2) = Icc((a1,b1),(a2,b2)).

LaTeX

$$Icc a1 a2 ×ˢ Icc b1 b2 = Icc (a1, b1) (a2, b2)$$

Lean4

@[simp]
theorem Icc_prod_Icc (a₁ a₂ : α) (b₁ b₂ : β) : Icc a₁ a₂ ×ˢ Icc b₁ b₂ = Icc (a₁, b₁) (a₂, b₂) :=
  by
  ext ⟨x, y⟩
  simp [and_assoc, and_left_comm]

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