instCountablePSigma — Mathlib

English

If α is countable and π(a) is countable for all a, then PSigma π is countable.

Русский

Если α счётно и все π(a) счётны, то PSigma π счётно.

LaTeX

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

Lean4

instance [Countable α] [∀ a, Countable (π a)] : Countable (PSigma π) :=
  Countable.of_equiv (Σ a : PLift α, PLift (π a.down)) (Equiv.psigmaEquivSigmaPLift π).symm

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