instCountableSum — Mathlib

English

If α and β are countable, then their sum α ⊕ β is countable.

Русский

Если α и β счётны, то сумма α ⊕ β счётна.

LaTeX

$$$$ \text{Countable}(\alpha) \land \text{Countable}(\beta) \Rightarrow \text{Countable}(\alpha \oplus \beta) $$$$

Lean4

instance [Countable α] [Countable β] : Countable (α ⊕ β) :=
  by
  rcases exists_injective_nat α with ⟨f, hf⟩
  rcases exists_injective_nat β with ⟨g, hg⟩
  exact (Equiv.natSumNatEquivNat.injective.comp <| hf.sumMap hg).countable

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