uIcc_prod_def — Mathlib

English

The uIcc interval in a product splits as a product of the corresponding uIcc intervals: uIcc(x,y) = uIcc(x1,y1) × uIcc(x2,y2).

Русский

Интервал uIcc в произведении распадается на произведение соответствующих интервалов uIcc: uIcc(x,y) = uIcc(x1,y1) × uIcc(x2,y2).

LaTeX

$$$ uIcc\,(x,y) = uIcc\,(x.1,y.1) \times\! uIcc\,(x.2,y.2) $$$

Lean4

theorem uIcc_prod_def (x y : α × β) : uIcc x y = uIcc x.1 y.1 ×ˢ uIcc x.2 y.2 :=
  rfl

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