topologicalClosure_eq_self — Mathlib

English

For a finite-dimensional subspace K, its topological closure equals itself when considered in a complete space.

Русский

Для конечномерного подпространства K его топологическое замыкание совпадает с самим K в аккуратно заданном пространстве.

LaTeX

$$$ K.topologicalClosure = K $$$

Lean4

@[simp]
theorem topologicalClosure_eq_self : K.topologicalClosure = K :=
  K.closed_of_finiteDimensional.submodule_topologicalClosure_eq

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