ofSubtype_subtypePerm_of_not_mem — Mathlib

English

If hg encodes p preservation by g and ha satisfies ¬p a, then extending the subtype-permutation fixes a.

Русский

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

LaTeX

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

Lean4

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

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