Theorems · Theorem · functional analysis

IsModuleTopology.continuous_bilinear_of_finite_left

∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : CommRing R] [IsTopologicalRing R] {A : Type u_2}
  [inst_3 : AddCommGroup A] [inst_4 : Module R A] [aA : TopologicalSpace A] [IsModuleTopology R A] {B : Type u_3}
  [inst_6 : AddCommGroup B] [inst_7 : Module R B] [aB : TopologicalSpace B] [IsModuleTopology R B] {C : Type u_4}
  [inst_9 : AddCommGroup C] [inst_10 : Module R C] [aC : TopologicalSpace C] [IsModuleTopology R C] [Module.Finite R A]
  (bil : A →ₗ[R] B →ₗ[R] C), Continuous fun ab => (bil ab.1) ab.2

If A, B and C have the module topology, and if furthermore A is a finite R-module, then any bilinear map A × B → C is automatically continuous

Defined in

Mathlib.Topology.Algebra.Module.ModuleTopology

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceCommRingIsTopologicalRingAddCommGroupModuleTopologicalSpaceIsModuleTopologyAddCommGroupModuleTopologicalSpaceIsModuleTopologyAddCommGroupModuleTopologicalSpaceIsModuleTopologyModule.Finite