inseparable_iff — Mathlib

English

In a space with a topological basis b, inseparability between x and y is characterized by x and y having identical membership patterns across all sets in b.

Русский

В пространстве с базисом b неразделимость x и y описывается тем, что их принадлежности во всех множествах из b совпадают.

LaTeX

$$$Inseparable(x,y) \iff \forall s \in b, x\in s \leftrightarrow y\in s.$$$

Lean4

theorem inseparable_iff {b : Set (Set X)} (hb : IsTopologicalBasis b) {x y : X} :
    Inseparable x y ↔ ∀ s ∈ b, (x ∈ s ↔ y ∈ s) :=
  ⟨fun h _ hs ↦ inseparable_iff_forall_isOpen.1 h _ (hb.isOpen hs), fun h ↦
    hb.nhds_hasBasis.eq_of_same_basis <| by
      convert hb.nhds_hasBasis using 2
      exact and_congr_right (h _)⟩

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