hasBasis_nhds_zero_of_basis — Mathlib

English

Under coherence and union conditions, the uniform convergence space is complete.

Русский

При когерентности и условиях объединения пространство равномерной конвергенции является полным.

LaTeX

$$$$ \text{CompleteSpace}(\mathrm{UniformConvergenceCLM}_{\sigma} F \mathfrak{S}) $$$$

Lean4

protected theorem hasBasis_nhds_zero_of_basis [TopologicalSpace F] [IsTopologicalAddGroup F] {ι : Type*} {p : ι → Prop}
    {b : ι → Set F} (h : (𝓝 0 : Filter F).HasBasis p b) :
    (𝓝 (0 : E →SL[σ] F)).HasBasis (fun Si : Set E × ι => IsVonNBounded 𝕜₁ Si.1 ∧ p Si.2) fun Si =>
      {f : E →SL[σ] F | ∀ x ∈ Si.1, f x ∈ b Si.2} :=
  UniformConvergenceCLM.hasBasis_nhds_zero_of_basis σ F {S | IsVonNBounded 𝕜₁ S} ⟨∅, isVonNBounded_empty 𝕜₁ E⟩
    (directedOn_of_sup_mem fun _ _ => IsVonNBounded.union) h

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