cl_eq_closure — Mathlib

English

For any A in Compactum, cl(A) equals the topological closure of A.

Русский

Замыкание множества A в Compactum совпадает с топологическим замыканием A.

LaTeX

$$$\\operatorname{cl}(A) = \\overline{A}$$$

Lean4

theorem cl_eq_closure {X : Compactum} (A : Set X) : cl A = closure A :=
  by
  ext
  rw [mem_closure_iff_ultrafilter]
  constructor
  · rintro ⟨F, h1, h2⟩
    exact ⟨F, h1, le_nhds_of_str_eq _ _ h2⟩
  · rintro ⟨F, h1, h2⟩
    exact ⟨F, h1, str_eq_of_le_nhds _ _ h2⟩

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