instIsCountablyGeneratedProdForallUniformityOfCountable

English

If ι is countable and each 𝓤(α i) is countably generated, then 𝓤(∀ i, α i) is countably generated.

Русский

Если индексовой набор ι счетен и каждая 𝓤(α_i) счетно порождает, то 𝓤(∀ i, α_i) тоже счетно порождается.

LaTeX

$$$[Countable ι] [\forall i, IsCountablyGenerated (\mathcal{U}(\alpha i))] \\Rightarrow IsCountablyGenerated (\mathcal{U}(\forall i, \alpha i))$$$

Lean4

instance [Countable ι] [∀ i, IsCountablyGenerated (𝓤 (α i))] : IsCountablyGenerated (𝓤 (∀ i, α i)) :=
  by
  rw [Pi.uniformity]
  infer_instance

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