Icc_product_Icc — Mathlib

English

The Cartesian product of two closed intervals equals the closed interval in the product order between the pair of endpoints.

Русский

Декартово произведение двух закрытых интервалов равно закрытому интервалу в порядке произведения между парами концов.

LaTeX

$$$ Icc a1 a2 \timesˢ Icc b1 b2 = Icc (a1,b1) (a2,b2) $$$

Lean4

theorem Icc_product_Icc (a₁ a₂ : α) (b₁ b₂ : β) : Icc a₁ a₂ ×ˢ Icc b₁ b₂ = Icc (a₁, b₁) (a₂, b₂) :=
  rfl

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