decidableMemRange — Mathlib

English

The cardinality of the range of subtypeCongrHom equals the cardinality of the product of permutation groups on subtype and its complement.

Русский

Мощность образа 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

instance decidableMemRange {α : Type*} (p : α → Prop) [DecidablePred p]
    [Fintype (Perm { a // p a } × Perm { a // ¬p a })] [DecidableEq (Perm α)] :
    DecidablePred (· ∈ (subtypeCongrHom p).range) := fun _ => inferInstance

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