mk_setProd — Mathlib

English

The cardinality of the Cartesian product s × t equals the product of the cardinalities: |s × t| = |s| · |t|.

Русский

Кардинальность декартового произведения s × t равна произведению кардинальностей |s| · |t|.

LaTeX

$$$|s \\times t| = |s| \\cdot |t|$$$

Lean4

@[simp]
theorem mk_setProd {α β : Type u} (s : Set α) (t : Set β) : #(s ×ˢ t) = #s * #t := by
  rw [mul_def, mk_congr (Equiv.Set.prod ..)]

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