English
If 𝓤 α is countably generated, there exists a sequence (V_n) of entourages forming a basis, all V_n symmetric.
Русский
Если униформность α счётно порождается, существует последовательность окружений (V_n), образующая базис, все V_n симметричны.
LaTeX
$$$\\exists V: \\mathbb{N} \\to \\mathcal{P}(α\\times α),\\ HasAntitoneBasis(\\mathcal{U}α, V) \\land \\forall n, IsSymmetricRel(V(n))$$$
Lean4
theorem nhds_eq_uniformity_prod {a b : α} :
𝓝 (a, b) = (𝓤 α).lift' fun s : Set (α × α) => {y : α | (y, a) ∈ s} ×ˢ {y : α | (b, y) ∈ s} :=
by
rw [nhds_prod_eq, nhds_nhds_eq_uniformity_uniformity_prod, lift_lift'_same_eq_lift']
· exact fun s => monotone_const.set_prod monotone_preimage
· refine fun t => Monotone.set_prod ?_ monotone_const
exact monotone_preimage (f := fun y => (y, a))
