English
In an ultra-uniform space, nhds has a basis given by symmetric and transitive entourages.
Русский
В ультра-равномерном пространстве окрестности имеют базис, задаваемый симметричными и транзитивными окружениями.
LaTeX
$$$\forall x: X,\ (\mathcal{N}_x) \text{ has basis of } \{V: IsSymmetricRel V \land IsTransitiveRel V \land V \in \mathcal{U}(X)\}$$$
Lean4
theorem mem_nhds_iff_symm_trans [IsUltraUniformity X] {x : X} {s : Set X} :
s ∈ 𝓝 x ↔ ∃ V ∈ 𝓤 X, IsSymmetricRel V ∧ IsTransitiveRel V ∧ UniformSpace.ball x V ⊆ s :=
by
rw [UniformSpace.mem_nhds_iff]
constructor
· rintro ⟨V, V_in, V_sub⟩
rw [IsUltraUniformity.hasBasis.mem_iff'] at V_in
obtain ⟨U, ⟨U_in, U_sym, U_trans⟩, U_sub⟩ := V_in
refine ⟨U, U_in, U_sym, U_trans, (UniformSpace.ball_mono U_sub _).trans V_sub⟩
· rintro ⟨V, V_in, _, _, V_sub⟩
exact ⟨V, V_in, V_sub⟩
