uIcc_prod_uIcc — Mathlib

English

In product spaces, the unordered interval between (a1, a2) and (b1, b2) equals the product of unordered intervals: [[a1, a2]] ×ˢ [[b1, b2]] = [[(a1, b1), (a2, b2)]]

Русский

В произведениях пространств неупорядоченная интервалировка между (a1, a2) и (b1, b2) равна произведению неупорядоченных интервалов: [[a1,a2]] ×ˢ [[b1,b2]] = [[(a1,b1),(a2,b2)]]

LaTeX

$$$ [[a_1,a_2]] \\timesˢ [[b_1,b_2]] = [[(a_1,b_1),(a_2,b_2)]] $$$

Lean4

@[simp]
theorem uIcc_prod_uIcc (a₁ a₂ : α) (b₁ b₂ : β) : [[a₁, a₂]] ×ˢ [[b₁, b₂]] = [[(a₁, b₁), (a₂, b₂)]] :=
  Icc_prod_Icc _ _ _ _

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