isCountablyGenerated_uniformity — Mathlib

English

If 𝓤 β is countably generated, then UniformOnFun.uniformity is countably generated whenever ht, hmono, and hex hold.

Русский

Если 𝓤 β счётно порождена, то равномерность UniformOnFun является счётно порождаемой при выполнении необходимых условий ht, hmono, hex.

LaTeX

$$$\text{If } (𝓤 β) \text{ is countably generated, then } 𝓤(α→ᵤ[𝔖]β) \text{ is countably generated under } ht,hmono,hex.$$$

Lean4

protected theorem isCountablyGenerated_uniformity [IsCountablyGenerated (𝓤 β)] {t : ℕ → Set α} (ht : ∀ n, t n ∈ 𝔖)
    (hmono : Monotone t) (hex : ∀ s ∈ 𝔖, ∃ n, s ⊆ t n) : IsCountablyGenerated (𝓤 (α →ᵤ[𝔖] β)) :=
  let ⟨_V, hV⟩ := exists_antitone_basis (𝓤 β)
  (UniformOnFun.hasAntitoneBasis_uniformity 𝔖 ht hmono hex hV).isCountablyGenerated

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