Theorems · Definition · functional analysis

ContinuousLinearMap.toSpanSingleton

(R₁ : Type u_1) →
  [inst : Semiring R₁] →
    {M₁ : Type u_4} →
      [inst_1 : TopologicalSpace M₁] →
        [inst_2 : AddCommMonoid M₁] →
          [inst_3 : Module R₁ M₁] → [inst_4 : TopologicalSpace R₁] → [ContinuousSMul R₁ M₁] → M₁ → R₁ →L[R₁] M₁

Given an element x of a topological space M over a semiring R, the natural continuous linear map from R to M by taking multiples of x.

Defined in

Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Cited by

133 results in Mathlib

Foundations

Depth 76 from the axioms, rests on 960 definitions · uses propext, Classical.choice, Quot.sound

Assumes

SemiringTopologicalSpaceAddCommMonoidModuleTopologicalSpaceContinuousSMul