countable_univ_pi — Mathlib

English

If α is finite and each s(a) is countable, then the product π(a) over a ∈ univ is countable when restricted to choices in s(a).

Русский

Если α конечно, и для каждого a множество s(a) счётно, то произведение из s(a) по a конечному индексу счётно.

LaTeX

$$$[\\text{Finite }\\alpha] \\to \\left( \\forall a, (s(a)).Countable \\right) \\Rightarrow (\\pi\\,\\mathrm{univ}\\, s).Countable$$$

Lean4

theorem countable_univ_pi {π : α → Type*} [Finite α] {s : ∀ a, Set (π a)} (hs : ∀ a, (s a).Countable) :
    (pi univ s).Countable :=
  have := fun a ↦ (hs a).to_subtype;
  .of_equiv _ (Equiv.Set.univPi s).symm

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