instCountableDFinsupp — Mathlib

English

If ι is countable and each α i is countable, then the dfinsupp Π₀ i, α i is countable.

Русский

Если ι счётно и каждый α i счётен, то DFinsupp Π₀ i, α i вещественно счётна.

LaTeX

$$$[\\text{Countable } \\iota] [\\forall i, \\text{Countable}(\\alpha i)] \\Rightarrow \\text{Countable}(\\Pi_0 i, \\alpha i)$$$

Lean4

instance [Countable ι] [∀ i, Countable (α i)] : Countable (Π₀ i, α i) := by
  classical
  let _ := Encodable.ofCountable ι
  let _ := fun i ↦ Encodable.ofCountable (α i)
  infer_instance

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