hasBasis_compactConvergenceUniformity

English

An entourage X is in the compact-convergence uniformity 𝓤(C(α,β)) iff it contains a set of the form { (f,g) | ∀ x ∈ K, (f x,g x) ∈ V } for some compact K and V ∈ 𝓤 β.

Русский

Любое окружение X в 𝓤(C(α,β)) содержит множество вида { (f,g) | ∀ x∈K, (f x,g x) ∈ V } для некоторого компактного K и V ∈ 𝓤 β.

LaTeX

$$$$ X \\in 𝓤(C(α,β)) \\iff ∃ K,V: IsCompact K ∧ V ∈ 𝓤 β ∧ {fg | ∀ x∈K, (fg.1 x, fg.2 x) ∈ V} \\subseteq X. $$$$

Lean4

theorem hasBasis_compactConvergenceUniformity :
    HasBasis (𝓤 C(α, β)) (fun p : Set α × Set (β × β) => IsCompact p.1 ∧ p.2 ∈ 𝓤 β) fun p =>
      {fg : C(α, β) × C(α, β) | ∀ x ∈ p.1, (fg.1 x, fg.2 x) ∈ p.2} :=
  (basis_sets _).compactConvergenceUniformity

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