Cardinality of the power set

Closed

Posted about 1 month ago · proven 20 days ago

Theorem & proof · powerset_card.lean · ✓ verified

1 2 3 4

import Mathlib

theorem powerset_card {α : Type*} [Fintype α] : Fintype.card (Set α) = 2 ^ Fintype.card α :=
  Fintype.card_set

Rewards pledged

No rewards pledged yet.