LinearMap.continuous_of_locally_bounded

theorem LinearMap.continuous_of_locally_bounded : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} {F : Type u_4} [inst : AddCommGroup E] [inst_1 : UniformSpace E] [inst_2 : UniformAddGroup E] [inst_3 : AddCommGroup F] [inst_4 : UniformSpace F] [inst_5 : FirstCountableTopology E] [inst_6 : RCLike 𝕜] [inst_7 : Module 𝕜 E] [inst_8 : ContinuousSMul 𝕜 E] [inst_9 : RCLike 𝕜'] [inst_10 : Module 𝕜' F] [inst_11 : ContinuousSMul 𝕜' F] {σ : 𝕜 →+* 𝕜'} [inst_12 : UniformAddGroup F] (f : E →ₛₗ[σ] F), (∀ (s : Set E), Bornology.IsVonNBounded 𝕜 s → Bornology.IsVonNBounded 𝕜' (⇑f '' s)) → Continuous ⇑f

This theorem states that given a locally bounded linear map `f` from `E` to `F` (denoted as `E →ₛₗ[σ] F`), if `E` is first countable, then `f` is continuous. Here, a set in `E` is called locally bounded if it is von Neumann bounded, which means that every neighborhood of 0 absorbs it. The condition of `E` being first countable is captured by the instance `FirstCountableTopology E`. The map `f` is continuous if for every set `s` in `E` that is von Neumann bounded, the image of `s` under `f` (`⇑f '' s`) is also von Neumann bounded in `F`. Other instances in the theorem statement specify additional properties of the types and operations involved, such as addition and scalar multiplication.

More concisely: Given a locally bounded linear map `f` from a first countable, von Neumann bounded set `E` to `F`, `f` is continuous.