powerset and subtypes

Stream: new members

[Bjørn Kjos-Hanssen]

Is there a way to connect the subtype {B // B ⊆ A} with the set A.powerset so as to prove the following?

variables {V : Type*} [decidable_eq V]
theorem card_and_subtype_difficulty (F : finset (finset V)) (A : finset V)
(φ : {B // B ⊆ A} → {C : finset V // C ∈ F}) :
function.injective φ →
A.powerset.card ≤ F.card :=
sorry

Or would it be possible to just directly say {B // B ⊆ A}).card ≤ {C : finset V // C ∈ F}.card somehow?

[Kevin Buzzard]

I'm not at lean right now but it seems to me that the result you want follows from more primitive results such as if f : X -> Y is injective then card X <= card Y and so on. What you seem to need is a bijection between your subtype and A.powerset. This bijection will have an explicit two-sided inverse so you can use equiv to do this. Is A.powerset really a set?

[Kevin Buzzard]

docs#finset.powerset

[Kevin Buzzard]

It's a finset so it can be promoted to a type and you could write down an equiv between it and your type of subsets. Will probably be slightly fiddly

[Bjørn Kjos-Hanssen]

Thanks @Kevin Buzzard . Maybe there's a way to avoid powerset altogether and just talk about cardinality of types?

[Kevin Buzzard]

Sure, there's something like docs#nat.card

[Bjørn Kjos-Hanssen]

Somehow I'm not able to import set_theory.fincard even though I can import set_theory.cardinal... and when I drop the set_theory.fincard file into my directory then it has errors like invalid field notation, 'to_nat' is not a valid "field" because environment does not contain 'cardinal.to_nat' mk α which has type cardinal

[Adam Topaz]

@Bjørn Kjos-Hanssen In case you're still stuck, here's a proof of your lemma:

import set_theory.cardinal
import data.finset.powerset

variables {V : Type*} [decidable_eq V]

theorem card_and_subtype_difficulty (F : finset (finset V)) (A : finset V)
(φ : {B // B ⊆ A} → {C : finset V // C ∈ F}) :
function.injective φ →
A.powerset.card ≤ F.card :=
begin
  intro h,
  suffices : (A.powerset.card : cardinal) ≤ F.card, by rwa cardinal.nat_cast_le at this,
  have : (A.powerset.card : cardinal) = cardinal.mk {B // B ⊆ A},
  { rw [cardinal.finset_card, cardinal.eq],
    refine ⟨⟨λ B, ⟨B, _⟩, λ B, ⟨B, _⟩, _, _⟩⟩,
    { cases B with B hB,
      rw finset.mem_powerset at hB, exact hB },
    { rw finset.mem_powerset, exact B.2 },
    { intro B, simp },
    { intro B, simp } },
  rw this, clear this,
  have : (F.card : cardinal) = cardinal.mk {C // C ∈ F},
  { rw [cardinal.finset_card, cardinal.eq],
    refine ⟨⟨λ B, ⟨B, B.2⟩, λ B, ⟨B, B.2⟩, λ B, by simp, λ B, by simp⟩⟩ },
  rw this, clear this,
  exact cardinal.mk_le_of_injective h,
end

This will also show you how to go between finset.card and cardinality, and the names of some lemmas that help proving that cardinals are equal.

[Adam Topaz]

This lemma can probably be golfed into just a few lines, but this proof is probably a bit more readable.

[Bjørn Kjos-Hanssen]

Oh my. I'll use this, and maybe with time start to understand it! For now I do get an error though, rewrite tactic failed, did not find instance of the pattern in the target expression ?m_2 ∈ powerset ?m_3 at the line rw finset.mem_powerset at hB, exact hB

[Adam Topaz]

Oh strange... Maybe I was using an old version of mathlib?

[Adam Topaz]

Let me double check...

[Adam Topaz]

No, it works for me just fine. Could be a namespace issue?

[Adam Topaz]

Are you using this in a large file with more imports perhaps?

[Adam Topaz]

E.g. there may be a conflict with docs#set.powerset and docs#finset.powerset if both the finset and set namespaces are open.

[Bjørn Kjos-Hanssen]

Actually I pasted your code in a blank file now and it has the same error. My installation of Lean, VS Code, mathlib etc. is from about a year ago if that helps.

[Bjørn Kjos-Hanssen]

But I see that your code works in the Lean Web Editor @Adam Topaz

[Adam Topaz]

Oh, you probably need to upgrade mathlib. Do you have mathlib-tools installed? If so, you can use the command leanproject upgrade-mathlib (but be prepared for some code to break if your current mathlib is ~1 year old)

[Adam Topaz]

Here's a reasonably golfed proof of this:

import set_theory.cardinal
import data.finset.powerset

variables {V : Type*} [decidable_eq V]

theorem card_and_subtype_difficulty (F : finset (finset V)) (A : finset V)
(φ : {B // B ⊆ A} → {C : finset V // C ∈ F}) :
function.injective φ →
A.powerset.card ≤ F.card :=
begin
  intro h,
  rw ← cardinal.nat_cast_le,
  convert cardinal.mk_le_of_injective h,
  { rw [cardinal.finset_card, cardinal.eq],
    exact ⟨⟨λ B, ⟨B, by simpa [finset.mem_powerset] using B.2⟩,
      λ B, ⟨B, by simpa [finset.mem_powerset] using B.2⟩, λ B, by simp, λ B, by simp⟩⟩ },
  { exact cardinal.finset_card },
end