subtypeEquivSubtypePerm — Mathlib

English

Permutations on a subtype are equivalent to permutations of α that fix pointwise the rest. More precisely, there is an equivalence between Perm(Subtype p) and { f : Perm α | ∀ a, ¬p a → f a = a }.

Русский

Перестановки подтипа эквивалентны перестановкам α, которые фиксируют точки вне подтипа. Формально существует эквиваленция Perm(Subtype p) ≃ { f : Perm α | ∀ a, ¬p a → f a = a }.

LaTeX

$$$ \\operatorname{Perm}(\\operatorname{Subtype} p) \\simeq \\{ f \\in \\operatorname{Perm}(\\alpha) \\;|\\; \\forall a, \\neg p(a) \\to f(a) = a \\}$$$

Lean4

/-- Permutations on a subtype are equivalent to permutations on the original type that fix pointwise
the rest. -/
@[simps]
protected def subtypeEquivSubtypePerm (p : α → Prop) [DecidablePred p] :
    Perm (Subtype p) ≃ { f : Perm α // ∀ a, ¬p a → f a = a }
    where
  toFun f := ⟨ofSubtype f, fun _ => f.ofSubtype_apply_of_not_mem⟩
  invFun
    f :=
    (f : Perm α).subtypePerm fun _ =>
      ⟨Decidable.not_imp_not.1 fun hfa => (f.prop _ hfa).symm ▸ hfa,
        Decidable.not_imp_not.1 fun hfa ha => hfa <| f.val.injective (f.prop _ hfa).symm ▸ ha⟩
  left_inv := Equiv.Perm.subtypePerm_ofSubtype
  right_inv f := Subtype.ext ((Equiv.Perm.ofSubtype_subtypePerm _) fun a => Not.decidable_imp_symm <| f.prop a)

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