English
The product neighborhood basis is given by symmetric entourages and s-prod decomposition.
Русский
База окрестностей произведения задаётся симметричными окружностями и разложением на s-продукт.
LaTeX
$$$\\text{HasBasis}(\\mathcal{N}(a,b), \\lambda s. s ∈ 𝓤 α ∧ \\mathrm{IsSymmetricRel}(s))\\; (s \\mapsto \\mathrm{ball}(a,s) \\times \\mathrm{ball}(b,s))$$$
Lean4
/-- Entourages are neighborhoods of the diagonal. -/
theorem nhds_le_uniformity (x : α) : 𝓝 (x, x) ≤ 𝓤 α :=
by
intro V V_in
rcases comp_symm_mem_uniformity_sets V_in with ⟨w, w_in, w_symm, w_sub⟩
have : ball x w ×ˢ ball x w ∈ 𝓝 (x, x) := by
rw [nhds_prod_eq]
exact prod_mem_prod (ball_mem_nhds x w_in) (ball_mem_nhds x w_in)
apply mem_of_superset this
rintro ⟨u, v⟩ ⟨u_in, v_in⟩
exact w_sub (mem_comp_of_mem_ball w_symm u_in v_in)
