card_preimage_mk — Mathlib

English

The cardinality of the preimage of a set under the quotient map equals the product of the cardinalities of the subgroup and the set.

Русский

Число элементов предобраза под отображением модуля деления равно произведению кардинальностей подгруппы и множества.

LaTeX

$$card (mk ⁻¹' t) = card s · card t$$

Lean4

theorem card_preimage_mk (s : Subgroup G) (t : Set (G ⧸ s)) :
    Nat.card (QuotientGroup.mk ⁻¹' t) = Nat.card s * Nat.card t := by
  rw [← Nat.card_prod, Nat.card_congr (preimageMkEquivSubgroupProdSet _ _)]

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