ofSubtype_apply_of_not_mem — Mathlib

English

If a does not satisfy p, then the extended permutation fixes a: the inclusion map sends a to itself when a ∉ p.

Русский

Если a не принадлежит к подтипу, то расширенная перестановка фиксирует a.

LaTeX

$$$ a \\notin p \\implies (\\mathrm{ofSubtype}\\, f)\\, a = a $$$

Lean4

theorem ofSubtype_apply_of_not_mem (f : Perm (Subtype p)) (ha : ¬p a) : ofSubtype f a = a :=
  extendDomain_apply_not_subtype _ _ ha

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