coe_product — Mathlib

English

The image of the product as a Set equals the product of the images as Sets: (s ×ˢ t) interpreted as a Set equals (s interpreted as Set) × (t interpreted as Set).

Русский

Образ произведения Finset как множества равен произведению соответствующих множеств.

LaTeX

$$$\uparrow(s \timesˢ t) = (s \uparrow) \times (t \uparrow)$$$

Lean4

@[simp, norm_cast]
theorem coe_product (s : Finset α) (t : Finset β) : (↑(s ×ˢ t) : Set (α × β)) = (s : Set α) ×ˢ t :=
  Set.ext fun _ => Finset.mem_product

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