of_finset_finset — Mathlib

English

If two finite sets are disjoint in a Hausdorff space, then they are separated in the sense of SeparatedNhds.

Русский

Пусть два конечных множества в Хаусдорфовом пространстве дисjoint; тогда они разделяются в смысле SeparatedNhds.

LaTeX

$$$\\forall X,[TopologicalSpace X], [T2Space X], s,t:\\ Finset X, Disjoint s t \\Rightarrow SeparatedNhds (s\\toSet) t.toSet$$$

Lean4

theorem of_finset_finset [T2Space X] (s t : Finset X) (h : Disjoint s t) : SeparatedNhds (s : Set X) t :=
  .of_isCompact_isCompact s.finite_toSet.isCompact t.finite_toSet.isCompact <| mod_cast h

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