Theorems · Definition · functional analysis

ContinuousLinearMap.proj

{R : Type u_1} →
  [inst : Semiring R] →
    {ι : Type u_4} →
      {φ : ι → Type u_5} →
        [inst_1 : (i : ι) → TopologicalSpace (φ i)] →
          [inst_2 : (i : ι) → AddCommMonoid (φ i)] →
            [inst_3 : (i : ι) → Module R (φ i)] → (i : ι) → ((i : ι) → φ i) →L[R] φ i

The projections from a family of topological modules are continuous linear maps.

Defined in

Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd

Cited by

77 results in Mathlib

Foundations

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

Assumes

SemiringTopologicalSpaceAddCommMonoidModule