Theorems · Theorem · functional analysis

LinearMap.continuous_of_finiteDimensional

∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] {F' : Type x} [inst_5 : AddCommGroup F']
  [inst_6 : Module 𝕜 F'] [inst_7 : TopologicalSpace F'] [IsTopologicalAddGroup F'] [ContinuousSMul 𝕜 F']
  [CompleteSpace 𝕜] [T2Space E] [FiniteDimensional 𝕜 E] (f : E →ₗ[𝕜] F'), Continuous ⇑f

Any linear map on a finite-dimensional space over a complete field is continuous.

Defined in

Mathlib.Topology.Algebra.Module.FiniteDimension

Cited by

17 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldAddCommGroupModuleTopologicalSpaceIsTopologicalAddGroupContinuousSMulAddCommGroupModuleTopologicalSpaceIsTopologicalAddGroupContinuousSMulCompleteSpaceT2SpaceFiniteDimensional