equivSubtypeMap_apply — Mathlib

English

The forward map of the equivalence p.equivSubtypeMap q on an element x is obtained by applying p.subtype.domRestrict to x.

Русский

Прямой образ эквивариантности p.equivSubtypeMap q к элементу x получается применением domRestrict к x.

LaTeX

$$$(p.equivSubtypeMap q)(x) = p.subtype.domRestrict q\,x$ for x in q.$$

Lean4

@[simp]
theorem equivSubtypeMap_apply {p : Submodule R M} {q : Submodule R p} (x : q) :
    (p.equivSubtypeMap q x : M) = p.subtype.domRestrict q x :=
  rfl

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