Submodules of normed groups #
@[implicit_reducible]
instance
Submodule.seminormedAddCommGroup
{𝕜 : Type u_1}
{E : Type u_2}
[Ring 𝕜]
[SeminormedAddCommGroup E]
[Module 𝕜 E]
(s : Submodule 𝕜 E)
:
A submodule of a seminormed group is also a seminormed group, with the restriction of the norm.
Equations
theorem
Submodule.norm_coe
{𝕜 : Type u_1}
{E : Type u_2}
[Ring 𝕜]
[SeminormedAddCommGroup E]
[Module 𝕜 E]
{s : Submodule 𝕜 E}
(x : ↥s)
:
If x is an element of a submodule s of a normed group E, its norm in E is equal to its
norm in s.
This is a reversed version of the simp lemma Submodule.coe_norm for use by norm_cast.
@[implicit_reducible]
instance
Submodule.normedAddCommGroup
{𝕜 : Type u_1}
{E : Type u_2}
[Ring 𝕜]
[NormedAddCommGroup E]
[Module 𝕜 E]
(s : Submodule 𝕜 E)
:
A submodule of a normed group is also a normed group, with the restriction of the norm.
Equations
- One or more equations did not get rendered due to their size.
theorem
LinearMap.continuous_domRestrict
{R : Type u_3}
{R' : Type u_4}
{M : Type u_5}
{M' : Type u_6}
[Semiring R]
[Semiring R']
[AddCommMonoid M]
[AddCommMonoid M']
[Module R M]
[Module R' M']
{σ₁₂ : R →+* R'}
(f : M →ₛₗ[σ₁₂] M')
[TopologicalSpace M]
[TopologicalSpace M']
(hf : Continuous ⇑f)
(p : Submodule R M)
:
Continuous ⇑(f.domRestrict p)