subtypeEquivSubtypePerm_apply_of_not_mem

English

If f is a permutation of the subtype and a ∉ p, then the α-component of the forward direction fixes a: (Perm.subtypeEquivSubtypePerm p f).1 a = a.

Русский

Если a не удовлетворяет p, то компонент α вправо эквивалентности фиксирует a.

LaTeX

$$$ (\\operatorname{Perm.subtypeEquivSubtypePerm} p\\, f).1\, a = a \\quad (ha: \\neg p(a)) $$$

Lean4

theorem subtypeEquivSubtypePerm_apply_of_not_mem (f : Perm (Subtype p)) (h : ¬p a) :
    ((Perm.subtypeEquivSubtypePerm p) f).1 a = a :=
  f.ofSubtype_apply_of_not_mem h

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