continuous_iff_isClosed_ker — Mathlib

English

For a linear map l: E → 𝕜, l is continuous iff its kernel is closed.

Русский

Для линейного отображения $l: E \to 𝕜$ непрерывность эквивалентна замкнутости ядра.

LaTeX

$$$\text{Continuous } l \iff IsClosed(\ker l)$$$

Lean4

/-- Any linear form on a topological vector space over a nontrivially normed field is continuous if
and only if its kernel is closed. -/
theorem continuous_iff_isClosed_ker (l : E →ₗ[𝕜] 𝕜) : Continuous l ↔ IsClosed (LinearMap.ker l : Set E) :=
  ⟨fun h => isClosed_singleton.preimage h, l.continuous_of_isClosed_ker⟩

Похожие утверждения