instHasCountableSeparatingOnIsClosedOfIsOpen

English

If s is T0 on its subspace and SecondCountable, there exists a countable family of open sets in X that separates points of s.

Русский

Пусть s — подмножество X, для которого удовлетворяются условия T0 на подпространстве и SecondCountable; существует счетное семейство открытых множества в X, разделяющее точки в s.

LaTeX

$$$\text{HasCountableSeparatingOn }(X, IsOpen, s)$$$

Lean4

/-- If there exists a countable family of open sets separating points of `s`, then there exists
a countable family of closed sets separating points of `s`. -/
instance [TopologicalSpace X] {s : Set X} [h : HasCountableSeparatingOn X IsOpen s] :
    HasCountableSeparatingOn X IsClosed s :=
  let ⟨S, hSc, hSo, hS⟩ := h.1
  ⟨compl '' S, hSc.image _, forall_mem_image.2 fun U hU ↦ (hSo U hU).isClosed_compl, fun x hx y hy h ↦
    hS x hx y hy fun _U hU ↦ not_iff_not.1 <| h _ (mem_image_of_mem _ hU)⟩

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