English
If B is finite as an R-module, then every bilinear map bil : A → B → C is continuous on A × B.
Русский
Если B конечно по отношению к модулю над R, то билинейная карта bil: A × B → C непрерывна на A × B.
LaTeX
$$$\\text{If } \\text{Module.Finite}(R,B) \\text{ and } bil: A \\to B \\to C,\\;\\ bil\\;\\text{is continuous on } A \\times B.$$$
Lean4
/-- If `A`, `B` and `C` have the module topology, and if furthermore `B` is a finite `R`-module,
then any bilinear map `A × B → C` is automatically continuous
-/
@[continuity, fun_prop]
theorem continuous_bilinear_of_finite_right [Module.Finite R B] (bil : A →ₗ[R] B →ₗ[R] C) :
Continuous (fun ab ↦ bil ab.1 ab.2 : (A × B → C)) := by
-- We already proved this when `A` is finite instead of `B`, so it's obvious by symmetry
rw [show
(fun ab ↦ bil ab.1 ab.2 : (A × B → C)) =
((fun ba ↦ bil.flip ba.1 ba.2 : (B × A → C)) ∘ (Prod.swap : A × B → B × A))
by ext; simp]
fun_prop
