ofSubtype_subtypePerm_of_mem — Mathlib

English

If hg encodes p preservation by g and ha satisfies p a, then extending the subtype-permutation of g to α agrees with g on a.

Русский

Если hg кодирует сохранение p перестановкой g и ha удовлетворяет p a, то продолжение подтип-перестановки g до α совпадает с g в точке a.

LaTeX

$$$ (\\mathrm{ofSubtype}(g.\\mathrm{subtypePerm}\\, hg))\\, a = g\\, a \\quad (ha:\\; p a) $$$

Lean4

theorem ofSubtype_subtypePerm_of_mem {p : α → Prop} [DecidablePred p] {g : Perm α} (hg : ∀ (x : α), p (g x) ↔ p x)
    {a : α} (ha : p a) : (ofSubtype (g.subtypePerm hg)) a = g a :=
  ofSubtype_apply_of_mem (g.subtypePerm hg) ha

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