card_range — Mathlib

English

The range size of sigmaCongrRightHom matches the range size of a product of permutation groups across the index family.

Русский

Размер образа sigmaCongrRightHom совпадает с размером образа произведения групп перестановок по индексу.

LaTeX

$$$\\mathrm{Fintype.card}(\\mathrm{range}(\\mathrm{sigmaCongrRightHom}\\,\\beta)) = \\mathrm{Fintype.card}(\\prod_{a} \\mathrm{Perm}(\\beta(a)))$$$

Lean4

@[simp]
theorem card_range {α : Type*} {β : α → Type*} [Fintype (sigmaCongrRightHom β).range] [Fintype (∀ a, Perm (β a))] :
    Fintype.card (sigmaCongrRightHom β).range = Fintype.card (∀ a, Perm (β a)) :=
  Fintype.card_eq.mpr ⟨(ofInjective (sigmaCongrRightHom β) sigmaCongrRightHom_injective).symm⟩

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