countable_pi — Mathlib

English

If α is finite and each s(a) is countable, then the set of functions f with f(a) ∈ s(a) for all a is countable.

Русский

Если α конечно и каждое s(a) счётно, то множество функций f с f(a) ∈ s(a) для всех a счётно.

LaTeX

$$$[\\text{Finite }\\alpha] \\Rightarrow \\left( \\forall a, (s(a)).Countable \\right) \\Rightarrow \\{ f: \\forall a, \\pi(a) \\mid \\forall a, f(a) \\in s(a)\\}.Countable$$$

Lean4

theorem countable_pi {π : α → Type*} [Finite α] {s : ∀ a, Set (π a)} (hs : ∀ a, (s a).Countable) :
    {f : ∀ a, π a | ∀ a, f a ∈ s a}.Countable := by simpa only [← mem_univ_pi] using countable_univ_pi hs

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