mem_compactConvergence_entourage_iff

English

A refined form of the previous criterion, with a simplification of the span of f,g by compact K and 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 mem_compactConvergence_entourage_iff (X : Set (C(α, β) × C(α, β))) :
    X ∈ 𝓤 C(α, β) ↔
      ∃ (K : Set α) (V : Set (β × β)),
        IsCompact K ∧ V ∈ 𝓤 β ∧ {fg : C(α, β) × C(α, β) | ∀ x ∈ K, (fg.1 x, fg.2 x) ∈ V} ⊆ X :=
  by simp [hasBasis_compactConvergenceUniformity.mem_iff, and_assoc]

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