English
A frequent pattern: the range of subtypeCongrHom has the same cardinality as a product of permutation ranges on subtypes.
Русский
Частый случай: образ subtypeCongrHom имеет ту же мощность, что и произведение образов перестановок подтипов.
LaTeX
$$$\\mathrm{Fintype.card}(\\mathrm{Subtype fun x => SetLike.instMembership.mem (\\mathrm{Equiv.Perm.subtypeCongrHom p}).range x)) = \\mathrm{Fintype.card}(\\mathrm{Perm}(\\text{Subtype } p) \\times \\mathrm{Perm}(\\text{Subtype } \\neg p))$$$
Lean4
@[simp]
theorem card_range {α : Type*} (p : α → Prop) [DecidablePred p] [Fintype (subtypeCongrHom p).range]
[Fintype (Perm { a // p a } × Perm { a // ¬p a })] :
Fintype.card (subtypeCongrHom p).range = Fintype.card (Perm { a // p a } × Perm { a // ¬p a }) :=
Fintype.card_eq.mpr ⟨(ofInjective (subtypeCongrHom p) (subtypeCongrHom_injective p)).symm⟩
