ofSubtype_apply_of_mem — Mathlib

English

For a permutation f of the subtype and a point a in α with p a, applying the inclusion map to a yields f evaluated at the corresponding subtype element ⟨a, ha⟩.

Русский

Для перестановки f над подтипом и точки a с p(a) возвращается значение f на представлении ⟨a, ha⟩ через включение.

LaTeX

$$$ (\\mathrm{ofSubtype}\\, f)\\, a = f\\langle a, ha\\rangle \\quad (ha:\\; p(a)) $$$

Lean4

theorem ofSubtype_apply_of_mem (f : Perm (Subtype p)) (ha : p a) : ofSubtype f a = f ⟨a, ha⟩ :=
  extendDomain_apply_subtype _ _ ha

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