card_mul — Mathlib

English

Let S and T be subsets of G such that every element of G can be written uniquely as a product s t with s ∈ S and t ∈ T. Then the cardinalities multiply to the cardinality of G: |S| · |T| = |G|.

Русский

Пусть S и T — подмножества G, для которых каждый элемент g ∈ G имеет единственную запись g = s t с s ∈ S, t ∈ T. Тогда кардинности удовлетворяют |S| · |T| = |G|.

LaTeX

$$$\mathrm{IsComplement}(S,T) \Rightarrow |S| \cdot |T| = |G|$$$

Lean4

theorem card_mul (h : IsComplement S T) : Nat.card S * Nat.card T = Nat.card G :=
  (Nat.card_prod _ _).symm.trans (Nat.card_eq_of_bijective _ h)

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