eq_of_uniformity_basis — Mathlib

English

Let α be a T0 space with a uniformity basis {s_i} and p_i. If x,y satisfy (x,y) ∈ s_i for all i with p_i, then x = y.

Русский

Пусть α — T0-пространство с базисом равномерности {s_i} и условиями p_i. Если для пары (x,y) выполняется (x,y) ∈ s_i для всех i, где p_i, то x = y.

LaTeX

$$$\forall i, p(i) \Rightarrow (x,y) \in s(i) \Rightarrow x = y$$$

Lean4

theorem eq_of_uniformity_basis {α : Type*} [UniformSpace α] [T0Space α] {ι : Sort*} {p : ι → Prop} {s : ι → Set (α × α)}
    (hs : (𝓤 α).HasBasis p s) {x y : α} (h : ∀ {i}, p i → (x, y) ∈ s i) : x = y :=
  (hs.inseparable_iff_uniformity.2 @h).eq

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