encard_prod — Mathlib

English

The encard of a Cartesian product equals the product of encards: encard(S × T) = encard(S) · encard(T).

Русский

Кардинальность encard сводится к произведению кардинальностей: encard(S × T) = encard(S) · encard(T).

LaTeX

$$$\operatorname{encard}(S \times T) = \operatorname{encard}(S) \cdot \operatorname{encard}(T)$$$

Lean4

@[simp]
theorem encard_prod {s : Set α} {t : Set β} : (s ×ˢ t).encard = s.encard * t.encard :=
  by
  unfold encard
  simp [ENat.card_congr (Equiv.Set.prod ..)]

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