Theorems · Definition · functional analysis

Pi.compRightL

(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)] → {α : Type u_6} → (f : α → ι) → ((i : ι) → φ i) →L[R] (i : α) → φ (f i)

Given a function f : α → ι, it induces a continuous linear function by right composition on product types. For f = Subtype.val, this corresponds to forgetting some set of variables.

Defined in

Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd

Cited by

8 results in Mathlib

Foundations

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

Assumes

SemiringTopologicalSpaceAddCommMonoidModule