Cartesian_Product_of_Countable_Sets_is_Countable
Provedcartesian-productcartesian-product-of-countable-sets-is-countablecountable-setsproofwikiset-theory
The cartesian product of two countable sets is countable.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Cartesian_Product_of_Countable_Sets_is_Countable (S T : Set ℕ) : Set.Countable (S ×ˢ T) := by sorry
Source