closure_eq_biUnion_inseparable — Mathlib

English

For a compact K in an R1-space X, the closure of K equals the union over x ∈ K of the sets { y | Inseparable x y }.

Русский

Для компактного K в R1-пространстве X замыкание K равно объединению по x∈K множеств {y | Inseparable x y}.

LaTeX

$$$ \\forall K [Set X], IsCompact K \\Rightarrow \\overline{K} = \\bigcup_{x\\in K} \\{ y \\mid Inseparable(x,y)\\}. $$$

Lean4

theorem closure_eq_biUnion_inseparable {K : Set X} (hK : IsCompact K) : closure K = ⋃ x ∈ K, {y | Inseparable x y} := by
  ext; simp [hK.mem_closure_iff_exists_inseparable]

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