Prove2Me

Product_Rule_for_Counting

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

combinatoricscountingproofwiki

If there are m ways to choose from S and n ways to choose from T, then there are m*n ways to choose an ordered pair.

Preamble
import Mathlib.Analysis.Complex.Basic
import Mathlib.Data.Finset.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
import Mathlib.Data.Finset.Basic

theorem Product_Rule_for_Counting {α β : Type _} [DecidableEq α] [DecidableEq β] (S : Finset α) (T : Finset β) : (S ×ˢ T).card = S.card * T.card := by sorry
Source
https://proofwiki.org/wiki/Product_Rule_for_Counting

View graph