hasBasis_compactConvergenceUniformity_of_compact

English

If β has a basis of uniformity with sets V, then the uniformity on C(α, β) has a basis indexed by V via precomposition, i.e., { (f, g) : ∀ x, (f x, g x) ∈ V }.

Русский

Если β имеет базис униформности с множествами V, то на C(α, β) базис униформности задаётся через V через пред-composition: пары отображений совпадают на всех x при условии (f x, g x) ∈ V.

LaTeX

$$$ (\mathcal{U} \beta) \text{ HasBasis } p V \Rightarrow (\mathcal{U} C(α, β)) \text{ HasBasis } p (λ i, \{fg : C(α, β) × C(α, β) \mid ∀ x, (fg.1 x, fg.2 x) ∈ V i\})$$$

Lean4

theorem hasBasis_compactConvergenceUniformity_of_compact :
    HasBasis (𝓤 C(α, β)) (fun V : Set (β × β) => V ∈ 𝓤 β) fun V ↦
      {fg : C(α, β) × C(α, β) | ∀ x, (fg.1 x, fg.2 x) ∈ V} :=
  hasBasis_compactConvergenceUniformity.to_hasBasis (fun p hp => ⟨p.2, hp.2, fun _fg hfg x _hx => hfg x⟩) fun V hV ↦
    ⟨⟨univ, V⟩, ⟨isCompact_univ, hV⟩, fun _fg hfg x => hfg x (mem_univ x)⟩

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