English
For any a,b in α, the product of neighborhood filters 𝓝 a × 𝓝 b equals a specified lift of the uniformity: 𝓝 a ×ˢ 𝓝 b = (𝓤 α).lift (λ s, (𝓤 α).lift' (λ t, {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ t})).
Русский
Для любых a,b ∈ α выполняется равенство 𝓝 a × 𝓝 b = (𝓤 α).lift (λ s, (𝓤 α).lift' (λ t, {y | (y, a) ∈ s} × {y | (b, y) ∈ t})).
LaTeX
$$$ 𝓝(a) \timesˢ 𝓝(b) = (\mathcal{U}(α)).lift \; (\lambda s : Set(α \times α), (\mathcal{U}(α)).lift'(\lambda t, \{ y : α \mid (y, a) \in s \} \timesˢ \{ y : α \mid (b, y) \in t \} )) $$$
Lean4
theorem nhds_nhds_eq_uniformity_uniformity_prod {a b : α} :
𝓝 a ×ˢ 𝓝 b = (𝓤 α).lift fun s : Set (α × α) => (𝓤 α).lift' fun t => {y : α | (y, a) ∈ s} ×ˢ {y : α | (b, y) ∈ t} :=
by
rw [nhds_eq_uniformity', nhds_eq_uniformity, prod_lift'_lift']
exacts [rfl, monotone_preimage, monotone_preimage]
