prod — Mathlib

English

The countable product of two countable sets is countable.

Русский

Счётное произведение двух счётных множеств счётно.

LaTeX

$$$\\forall s:\\ Set\\alpha, \\forall t:\\ Set\\beta,\\sqrt{\\ }(s.Countable) \\land (t.Countable) \\Rightarrow (s\\times t).Countable$$$

Lean4

protected theorem prod {s : Set α} {t : Set β} (hs : s.Countable) (ht : t.Countable) : Set.Countable (s ×ˢ t) :=
  have := hs.to_subtype;
  have := ht.to_subtype;
  .of_equiv _ <| (Equiv.Set.prod _ _).symm

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