English
The nhds of x is symmetric with respect to symmetric relations: s ∈ nhds x iff there exists symmetric V with ball x V ⊆ s.
Русский
Окрестности x симметричны по отношению к симметричнымRelation: s ∈ nhds x эквивалентно существованию симметричного V с ball x V ⊆ s.
LaTeX
$$$s \in \mathcal N(x) \iff \exists V \in \mathcal U(\alpha), IsSymmetricRel V \land ball(x,V) \subseteq s$$$
Lean4
theorem mem_nhds_iff_symm {x : α} {s : Set α} : s ∈ 𝓝 x ↔ ∃ V ∈ 𝓤 α, IsSymmetricRel V ∧ ball x V ⊆ s :=
by
rw [UniformSpace.mem_nhds_iff]
constructor
· rintro ⟨V, V_in, V_sub⟩
use symmetrizeRel V, symmetrize_mem_uniformity V_in, symmetric_symmetrizeRel V
exact Subset.trans (ball_mono (symmetrizeRel_subset_self V) x) V_sub
· rintro ⟨V, V_in, _, V_sub⟩
exact ⟨V, V_in, V_sub⟩
