Theorems · Definition · functional analysis

Submodule.subtypeL

{R : Type u_1} →
  [inst : Semiring R] →
    {M : Type u_2} →
      [inst_1 : TopologicalSpace M] →
        [inst_2 : AddCommMonoid M] → [inst_3 : Module R M] → (p : Submodule R M) → ↥p →L[R] M

Submodule.subtype as a ContinuousLinearMap.

Defined in

Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict

Cited by

53 results in Mathlib

Foundations

Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringTopologicalSpaceAddCommMonoidModule