cardinality of powerset of finite sets

Stream: Is there code for X?

[Sabbir Rahman]

Is there a theorem stating cardinality of powerset of finite sets is 2^card? In particular this

import Mathlib

universe u

example (α : Type u) (s : Set α) (hf: s.Finite) : (𝒫 s).ncard = 2 ^ (s.ncard) := by
  sorry

I have found Finset.card_powerset and Multiset.card_powerset, but no such thing for sets.

[Kevin Buzzard]

You can hopefully deduce it fairly easily from the Finset version if it's not there (and PR it!)

[Yaël Dillies]

Exercise for you: answer your own question using https://loogle.lean-lang.org/ :wink:

[Sabbir Rahman]

Yeah I always try loogle first, but there have been several times where i have missed something due to not knowing definitions or possible pattern or naming patterns. Then I ask on zulip

[Yaël Dillies]

Ah sure. In this case, things are pretty plain and I would expect Loogle to be trustworthy

[Timo Carlin-Burns]

To be clear, the answer is that no lemma relating Set.encard and Set.powerset exists: https://loogle.lean-lang.org/?q=Set.ncard%2C+Set.powerset

[Sabbir Rahman]

So powerset cardinality is not in mathlib, but there are related things, from them I could figure out two proofs

import Mathlib

universe u
variable {α : Type u}

example  (s : Set α) (hs : s.Finite) : (𝒫 s).ncard = 2 ^ (s.ncard) := by
  have h := Cardinal.mk_powerset s
  rw [← Set.cast_ncard hs.powerset, ← Set.cast_ncard hs] at h
  norm_cast at h

example  (s : Set α) (hs : s.Finite) : (𝒫 s).ncard = 2 ^ (s.ncard) := by
  obtain ⟨s', hs'⟩ := hs.exists_finset_coe
  rw [← hs', Set.ncard_coe_Finset, ← Finset.card_powerset, ← Set.ncard_coe_Finset, Finset.coe_powerset, eq_comm]
  apply Set.ncard_preimage_of_injective_subset_range
  . rintro a b hab
    norm_cast at hab
  . rintro ss hss
    obtain ⟨ss', hss'⟩ := s'.finite_toSet |>.subset hss |>.exists_finset_coe
    simp [← hss']

one proof uses finset, one proof uses Cardinal. I guess they are independent. to create a pr, which is more mathlib-natural?