eq_of_forall_symmetric — Mathlib

English

If for every symmetric entourage V in 𝓤α we have (x,y) ∈ V, then x = y.

Русский

Если для каждого симметричного окружения V в 𝓤α выполняется (x,y) ∈ V, то x = y.

LaTeX

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

Lean4

theorem eq_of_forall_symmetric {α : Type*} [UniformSpace α] [T0Space α] {x y : α}
    (h : ∀ {V}, V ∈ 𝓤 α → IsSymmetricRel V → (x, y) ∈ V) : x = y :=
  eq_of_uniformity_basis hasBasis_symmetric (by simpa)

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