ofSubtype_apply_coe — Mathlib

English

For a permutation f of the subtype and a subtype element x, the inclusion map sends x to the same value as f acting on x itself (via the ambient α).

Русский

Для перестановки f подтипа и элемента x подтипа включение отправляет x в то же значение, что и f действует на x через окружение α.

LaTeX

$$$ (\\mathrm{ofSubtype}\\, f)\, x = f\, x \quad (x \\in \\operatorname{Subtype}(p)) $$$

Lean4

@[simp]
theorem ofSubtype_apply_coe (f : Perm (Subtype p)) (x : Subtype p) : ofSubtype f x = f x :=
  Subtype.casesOn x fun _ => ofSubtype_apply_of_mem f

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