equivSubtypeMap_symm_apply — Mathlib

English

The inverse of the equivalence p.equivSubtypeMap q sends an element of q.map p.subtype back to a corresponding element in q.

Русский

Обратное отображение эквивSubtypeMap возвращает элемент из q.map p.subtype в q.

LaTeX

$$$(p.equivSubtypeMap q)^{-1}(x) = x\\quad\\text{for } x \\in q.map p.subtype$$$

Lean4

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

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