BarrelledSpace.continuous_of_lowerSemicontinuous

theorem BarrelledSpace.continuous_of_lowerSemicontinuous : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : AddGroup E] [inst_2 : SMul 𝕜 E] [inst_3 : TopologicalSpace E] [self : BarrelledSpace 𝕜 E] (p : Seminorm 𝕜 E), LowerSemicontinuous ⇑p → Continuous ⇑p

The theorem states that in a barrelled space, all lower semicontinuous seminorms on `E` are actually continuous. Simply put, if `p` is a seminorm on a space `E` over a seminormed ring `𝕜`, and if the function mapping from `E` to its seminorm value is lower semicontinuous, then this function is also continuous. Here, a function is lower semicontinuous if, for any point `x` and any value `y` less than the function value at `x`, there exists a neighborhood of `x` such that the function value at any point in the neighborhood is greater than `y`. A barrelled space is a topological vector space for which every barrelled subset is a neighborhood of the zero vector.

More concisely: In a barrelled space, every lower semicontinuous seminorm is continuous.