Theorems · Definition · functional analysis

ContinuousLinearMap.id

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

the identity map as a continuous linear map.

Defined in

Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Cited by

233 results in Mathlib

Foundations

Depth 18 from the axioms, rests on 174 definitions · uses no axioms

Assumes

SemiringTopologicalSpaceAddCommMonoidModule