English
A linear form on a topological vector space over a nontrivially normed field is continuous if it is nonzero on some nonempty open set and the kernel is closed.
Русский
Линейная форма на топологическом векторном пространстве над ненулевым нормированным полем непрерывна, если она не равна нулю на некотором не пустом открытом множестве и ядро замкнуто.
LaTeX
$$Theorem: if l is a linear form with IsClosed ker(l) and l nonzero on some open set, then l is continuous.$$
Lean4
/-- Over a nontrivially normed field, any linear form which is nonzero on a nonempty open set is
automatically continuous. -/
theorem continuous_of_nonzero_on_open (l : E →ₗ[𝕜] 𝕜) (s : Set E) (hs₁ : IsOpen s) (hs₂ : s.Nonempty)
(hs₃ : ∀ x ∈ s, l x ≠ 0) : Continuous l :=
by
refine l.continuous_of_isClosed_ker (l.isClosed_or_dense_ker.resolve_right fun hl => ?_)
rcases hs₂ with ⟨x, hx⟩
have : x ∈ interior (LinearMap.ker l : Set E)ᶜ :=
by
rw [mem_interior_iff_mem_nhds]
exact mem_of_superset (hs₁.mem_nhds hx) hs₃
rwa [hl.interior_compl] at this
