English
If α is finite and each π(a) is countable, then the space of all functions a → π(a) is countable.
Русский
Если α конечен и для каждого a π(a) счётно, то множество функций a → π(a) счётно.
LaTeX
$$$ \operatorname{Finite}(\alpha) \land \forall a, \operatorname{Countable}(\pi(a)) \Rightarrow \operatorname{Countable}\big((a : \alpha) \to \pi(a)\big) $$$
Lean4
instance [Finite α] [∀ a, Countable (π a)] : Countable (∀ a, π a) :=
by
have (n : ℕ) : Countable (Fin n → ℕ) := by
induction n with
| zero => infer_instance
| succ n ihn => exact Countable.of_equiv (ℕ × (Fin n → ℕ)) (Fin.consEquiv fun _ ↦ ℕ)
rcases Finite.exists_equiv_fin α with ⟨n, ⟨e⟩⟩
have f := fun a => (nonempty_embedding_nat (π a)).some
exact ((Embedding.piCongrRight f).trans (Equiv.piCongrLeft' _ e).toEmbedding).countable
