closed_of_finiteDimensional — Mathlib

English

If an affine subspace s of a normed space has finite-dimensional direction, then s is a closed subset.

Русский

В нормированном пространстве аффинное подпространство s, чьё направление конечномерно, является замкнутым подмножеством.

LaTeX

$$$[FiniteDimensional 𝕜 (s.direction)] \\\\Rightarrow IsClosed ((s : Set P))$$$

Lean4

theorem closed_of_finiteDimensional {P : Type*} [MetricSpace P] [NormedAddTorsor E P] (s : AffineSubspace 𝕜 P)
    [FiniteDimensional 𝕜 s.direction] : IsClosed (s : Set P) :=
  s.isClosed_direction_iff.mp s.direction.closed_of_finiteDimensional

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