card_mul_iff — Mathlib

English

The equality |s*t| = |s|·|t| holds iff the map (x,y) ↦ x*y is injective on s×t.

Русский

Равенство кардинал |s*t| = |s|·|t| выполняется тогда и только тогда, когда отображение (x,y) ↦ x*y инъективно на s×t.

LaTeX

$$$|s * t| = |s| \\cdot |t| \iff (s \timesˢ t : Set (\\alpha × \\alpha)).InjOn (\\fun p => p.1 * p.2)$$$

Lean4

@[to_additive]
theorem card_mul_iff : #(s * t) = #s * #t ↔ (s ×ˢ t : Set (α × α)).InjOn fun p => p.1 * p.2 :=
  card_image₂_iff

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