isClosed — Mathlib

English

In a separated uniform space, every complete subset is closed.

Русский

В разделимом равномерном пространстве каждоe полное множество замкнуто.

LaTeX

$$$\\forall \\alpha\\, [UniformSpace\\alpha]\\,[T0Space\\alpha],\\, \\forall s\\subseteq \\alpha,\\ IsComplete(s)\\Rightarrow IsClosed(s)$$$

Lean4

/-- In a separated space, a complete set is closed. -/
theorem isClosed [UniformSpace α] [T0Space α] {s : Set α} (h : IsComplete s) : IsClosed s :=
  isClosed_iff_clusterPt.2 fun a ha => by
    let f := 𝓝[s] a
    have : Cauchy f := cauchy_nhds.mono' ha inf_le_left
    rcases h f this inf_le_right with ⟨y, ys, fy⟩
    rwa [(tendsto_nhds_unique' ha inf_le_left fy : a = y)]

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