instCountableProd — Mathlib

English

If α and β are countable, then α × β is countable.

Русский

Если A и B счётны, то A × B счётно.

LaTeX

$$$ \operatorname{Countable}(\alpha) \land \operatorname{Countable}(\beta) \rightarrow \operatorname{Countable}(\alpha \times \beta) $$$

Lean4

instance [Countable α] [Countable β] : Countable (α × β) :=
  by
  rcases exists_injective_nat α with ⟨f, hf⟩
  rcases exists_injective_nat β with ⟨g, hg⟩
  exact (Nat.pairEquiv.injective.comp <| hf.prodMap hg).countable

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