submoduleMap — Mathlib

English

For any hpq : p = q and x ∈ p, the coerce of the equality-based isometry sends x to itself in E.

Русский

Для любого hpq: p = q и x ∈ p, отображение через коегерентное преобразование отправляет x в сам x в E.

LaTeX

$$$hpq : p = q \;\; x \in p \Rightarrow ((ofEq(p,q,hpq)\,x) : E) = x$$$

Lean4

/-- A linear isometry equivalence between two modules restricts to a
linear isometry equivalence from any submodule `p` of the domain onto
the image of that submodule.

This is a version of `LinearEquiv.submoduleMap` extended to linear isometry equivalences. -/
@[simps!]
def submoduleMap (p : Submodule R M) (e : M ≃ₛₗᵢ[σ₁₂] M₂) : p ≃ₛₗᵢ[σ₁₂] (Submodule.map e p) :=
  { e.toLinearEquiv.submoduleMap p with norm_map' x := e.norm_map' x }

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