nhds_eq — Mathlib

English

A variant: for 𝔖 and a basis hb for 𝓤 β, the nhds of f in α →ᵤ[𝔖] β equals an infimum involving basis elements, i.e., 𝓝 f = ⨅ S∈𝔖 ⨅ i with hb, 𝓟 {g : ∀ x ∈ S, (f x, g x) ∈ V_i}.

Русский

Вариант: для 𝔖 и базиса hb для 𝓤 β, 𝓝 f = ⨅ S∈𝔖 ⨅ i, 𝓟 {g: ∀ x∈S, (f x, g x) ∈ V_i}.

LaTeX

$$$\text{nhds}(f) = ⨅ S∈𝔖 ⨅ i, 𝓟\{g: ∀ x∈S, (f x, g x) ∈ V_i\}$.$$

Lean4

protected theorem nhds_eq (f : α →ᵤ[𝔖] β) : 𝓝 f = ⨅ s ∈ 𝔖, ⨅ V ∈ 𝓤 β, 𝓟 {g | ∀ x ∈ s, (toFun 𝔖 f x, toFun 𝔖 g x) ∈ V} :=
  UniformOnFun.nhds_eq_of_basis _ _ (𝓤 β).basis_sets f

Похожие утверждения