uIcc_product_uIcc — Mathlib

English

The cardinality of the uIcc interval grows multiplicatively over the product: card(uIcc(x,y)) = card(uIcc(x1,y1)) · card(uIcc(x2,y2)).

Русский

Кардинал интервала uIcc в произведении множится: card(uIcc(x,y)) = card(uIcc(x1,y1)) · card(uIcc(x2,y2)).

LaTeX

$$$ \#(uIcc\,(x,y)) = \#(uIcc\,(x.1,y.1)) \cdot \#(uIcc\,(x.2,y.2)) $$$

Lean4

theorem uIcc_product_uIcc (a₁ a₂ : α) (b₁ b₂ : β) : uIcc a₁ a₂ ×ˢ uIcc b₁ b₂ = uIcc (a₁, b₁) (a₂, b₂) :=
  rfl

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