compactConvergenceUniformity_of_compact

English

If α is compact and 𝒰β has a basis given by p and V, then 𝒰C(α, β) has basis given by the same p and the family { fg : C(α, β) × C(α, β) | ∀ x, (fg.1 x, fg.2 x) ∈ V_i }.

Русский

Пусть α компактно и 𝒰β имеет базис p и V. Тогда униформность C(α, β) имеет базис, задаваемый тем же p и семейством множеств { fg : C(α, β) × C(α, β) | ∀ x, (fg.1 x, fg.2 x) ∈ V_i }.

LaTeX

$$$ (g \in C(β, δ)) (hg : UniformContinuous g) : UniformContinuous (ContinuousMap.comp g) $; [приведём через униформизацию] $$

Lean4

theorem _root_.Filter.HasBasis.compactConvergenceUniformity_of_compact {ι : Sort*} {p : ι → Prop} {V : ι → Set (β × β)}
    (h : (𝓤 β).HasBasis p V) : HasBasis (𝓤 C(α, β)) p fun i ↦ {fg : C(α, β) × C(α, β) | ∀ x, (fg.1 x, fg.2 x) ∈ V i} :=
  hasBasis_compactConvergenceUniformity_of_compact.to_hasBasis
    (fun _U hU ↦ (h.mem_iff.mp hU).imp fun _i ⟨hpi, hi⟩ ↦ ⟨hpi, fun _ h a ↦ hi <| h a⟩) fun i hi ↦
    ⟨V i, h.mem_of_mem hi, .rfl⟩

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