uniformity_eq — Mathlib

English

For f ∈ UniformOnFun α β 𝔖, the neighbourhood filter 𝓝 f equals the infimum over S ∈ 𝔖 and V ∈ 𝓤 β of principal filters generated by UniformOnFun.gen 𝔖 S V.

Русский

Для f ∈ UniformOnFun α β 𝔖 окрестности 𝓝 f равны пересечению по S∈𝔖 и V∈𝓤 β базисных фильтров, порождаемых UniformOnFun.gen 𝔖 S V.

LaTeX

$$$\mathcal N(f) = \bigwedge_{S∈𝔖} \bigwedge_{V∈𝓤 β} \mathcal P (UniformOnFun.gen 𝔖 S V).$$$

Lean4

protected theorem uniformity_eq : 𝓤 (α →ᵤ[𝔖] β) = ⨅ s ∈ 𝔖, ⨅ V ∈ 𝓤 β, 𝓟 (UniformOnFun.gen 𝔖 s V) :=
  UniformOnFun.uniformity_eq_of_basis _ _ (𝓤 β).basis_sets

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