coe_prod — Mathlib

English

The carrier of the product of K and L equals the product of their carriers: (K.prod L : Set (α × β)) = (K : Set α) ×ˢ (L : Set β).

Русский

Носитель произведения K и L равен произведению носителей: (K.prod L : Set (α × β)) = (K : Set α) ×ˢ (L : Set β).

LaTeX

$$$\\forall {K : \\mathrm{Compacts}(\\alpha)} {L : \\mathrm{Compacts}(\\beta)},\\\\ (K.prod L : \\text{Set }(\\alpha \\times \\beta)) = (K : \\text{Set }\\alpha) \\times^{\\!} (L : \\text{Set }\\beta)$$$

Lean4

@[simp]
theorem coe_prod (K : Compacts α) (L : Compacts β) : (K.prod L : Set (α × β)) = (K : Set α) ×ˢ (L : Set β) :=
  rfl

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