exists_mem_of_ne — Mathlib

English

For any topological basis b in a space X that is T1, and any distinct x,y in X, there exists a basis element a ∈ b such that x ∈ a and y ∉ a.

Русский

Для любой базисной системы b в пространстве X, которое удовлетворяет условиям T1, и для любых различных x,y ∈ X, существуют a ∈ b такое, что x ∈ a и y ∉ a.

LaTeX

$$$\\forall X [\\mathcal{T}_1(X)], \\forall \\text{hb IsTopologicalBasis } b, \\forall x,y, x\\neq y \\Rightarrow \\exists a\\in b, x\\in a \\land y\\notin a.$$$

Lean4

theorem exists_mem_of_ne [T1Space X] {b : Set (Set X)} (hb : IsTopologicalBasis b) {x y : X} (h : x ≠ y) :
    ∃ a ∈ b, x ∈ a ∧ y ∉ a := by
  rcases hb.isOpen_iff.1 isOpen_ne x h with ⟨a, ab, xa, ha⟩
  exact ⟨a, ab, xa, fun h => ha h rfl⟩

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