eq_of_uniformity — Mathlib

English

If every entourage contains a given pair (x, y), then x equals y (in a T0 space).

Русский

Если для каждой окрестности содержится пара (x, y), тогда x = y (в T0-пространстве).

LaTeX

$$$\forall V\in 𝓤(α), (x,y) \in V \Rightarrow x = y$$$

Lean4

theorem eq_of_uniformity {α : Type*} [UniformSpace α] [T0Space α] {x y : α} (h : ∀ {V}, V ∈ 𝓤 α → (x, y) ∈ V) : x = y :=
  t0Space_iff_uniformity.mp ‹T0Space α› x y @h

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