Theorems · Definition · functional analysis

Equiv.continuousLinearEquiv

(R : Type u_1) →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : TopologicalSpace β] →
        [inst_1 : AddCommMonoid β] → [inst_2 : Semiring R] → [inst_3 : Module R β] → (e : α ≃ β) → α ≃L[R] β

An equivalence e : α ≃ β gives a continuous linear equivalence α ≃L[R] β where the continuous R-module structure on α is the one obtained by transporting an R-module structure on β back along e. This is e.linearEquiv as a continuous linear equivalence.

Defined in

Mathlib.Topology.Algebra.Module.TransferInstance

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceAddCommMonoidSemiringModule