Theorems · Definition · functional analysis

ContinuousLinearEquiv.funUnique

(ι : Type u_1) →
  (R : Type u_2) →
    (M : Type u_3) →
      [Unique ι] →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → [inst_3 : TopologicalSpace M] → (ι → M) ≃L[R] M

If ι has a unique element, then ι → M is continuously linear equivalent to M.

Defined in

Mathlib.Topology.Algebra.Module.Equiv

Cited by

3 results in Mathlib

Foundations

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

Assumes

UniqueSemiringAddCommMonoidModuleTopologicalSpace