uIcc_prod_eq — Mathlib

English

The unordered interval of a pair equals the unordered intervals componentwise: [[a, b]] = [[a1, b1]] ×ˢ [[a2, b2]] for a=(a1,a2), b=(b1,b2).

Русский

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

LaTeX

$$$ [[a,b]] = [[a.1,b.1]] \\timesˢ [[a.2,b.2]] $$$

Lean4

theorem uIcc_prod_eq (a b : α × β) : [[a, b]] = [[a.1, b.1]] ×ˢ [[a.2, b.2]] := by simp

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