instCountableSigma — Mathlib

English

If α is countable and each π(a) is countable, then the Sigma-type Σ π is countable.

Русский

Если α счётно и каждый π(a) счётен, то сигма-тип Σ π счётен.

LaTeX

$$$ \operatorname{Countable}(\alpha) \land \forall a, \operatorname{Countable}(\pi(a)) \Rightarrow \operatorname{Countable}(\Sigma \pi) $$$

Lean4

instance [Countable α] [∀ a, Countable (π a)] : Countable (Sigma π) :=
  by
  rcases exists_injective_nat α with ⟨f, hf⟩
  choose g hg using fun a => exists_injective_nat (π a)
  exact ((Equiv.sigmaEquivProd ℕ ℕ).injective.comp <| hf.sigma_map hg).countable

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