Powerset of Fintype

Stream: new members

[Angelo Lucia]

When we have a set of a Fintype, there seems to be 4 different ways to talk about its powerset:

import Mathlib.Data.Fintype.Powerset
import Mathlib.Data.Finset.Powerset

universe u
open Classical
variable {V : Type u} [Fintype V] (s : Set V)

#check 𝒫 s -- Set (Set V)
#check (𝒫 s).toFinset -- Finset (Set V)
#check s.toFinset.powerset -- Finset (Finset V)
#check s.toFinset.powerset.toSet -- Set (Finset V)

If I have an element of one of these 4, I can easily write an explicit conversion to any of the three other, usually as something like this:

variable (F : s.toFinset.powerset)
noncomputable example : 𝒫 s := ⟨F.val, by {
  let ⟨f, h⟩ := F
  simp at h
  simp
  exact h
  }⟩

Is there a more compact way to do this instead of having to do it "by hand" explicitly?

[Yaël Dillies]

Sounds like a #xy problem. Why do you want to take an element of the powerset coerced to a type? namely why do you have F : s.toFinset.powerset instead of F + F ∈ s.toFinset.powerset?

[Edward van de Meent]

or maybe just F and F ⊆ s?

[Yaël Dillies]

You spoiled the second part of my explanation, but yes you are right :wink:

[Edward van de Meent]

what second part? :upside_down:

[Yaël Dillies]

(I was waiting for an answer from Angelo)

[Angelo Lucia]

Sorry I am trying to clarify where I am coming from with some example, but it is taking some time :smile:

[Angelo Lucia]

I am trying to use the BigOperator notation to take sums and products over Finsets.

If I want to sum over elements of 𝒫 s a certain function g, it seems more convenient to write it as ∑ (F : 𝒫 s), g F, since writing it this way allows me to have g : 𝒫 s → ℕ, i.e. only defined on subsets of s. Writing it as∑ {F | F ⊆ s}, g F or ∑ F ∈ 𝒫 s, g F seems to require g to be defined over Set V.

But then if I want to apply Finset.prod_add for example, I would end up with something like

∏ i ∈ s, (f i + g i) = ∑ t ∈ s.powerset, (∏ i ∈ t, f i) * ∏ i ∈ s \ t, g i

and that sum over s.powerset I believe is equivalent to (𝒫 s).toFinset. So in order to apply this theorem I would need my functions to be defined on the "whole" Set V.

I was trying to figure out a way to avoid this, but maybe I am trying to solve this the wrong way around.

[Angelo Lucia]

Maybe more generally, I am confused about the following: when summing over a finset defined by a property, is there a way to get that the information about the property "inside the sum"?

∑ F ∈ { F | p F}, g F -- how to I access the fact that p F holds true in here?

[Edward van de Meent]

this setup works:

import Mathlib
open BigOperators

variable (α : Type*) [Fintype α] (p : Set α → Prop) (g : (s:Set α) → p s → Nat )

#check ∑ F, ∑ᶠ h:p F, g F h

[Edward van de Meent]

although honestly i do agree that this notation is a tad annoying to work with, particularly when you only know that {F | p F} is finite, rather than Fintype α

[Edward van de Meent]

(in the sense that this doesn't work in that case)

[Angelo Lucia]

I see. Thanks, I was not aware of ∑ᶠ . It seems one can also write it directly as

#check ∑ᶠ (F : Set V) (h : F ⊆ s), g F h

which avoids the confusing double summation symbol. I guess this is the closest thing to ∑ (F : 𝒫 s) avoiding the coercion to a type.

[Ruben Van de Velde]

import Mathlib

variable (p : X → Prop) [Fintype X] (g : (x : X) → p x → ℕ)

-- Not sure what's up here
noncomputable instance : Fintype { F : X // p F} := by exact Fintype.ofFinite { F // p F }

#check ∑ F : { F : X // p F }, g F F.prop -- how to I access the fact that p F holds true in here?

[Angelo Lucia]

Ruben Van de Velde ha scritto:

#check ∑ F : { F : X // p F }, g F F.prop -- how to I access the fact that p F holds true in here?

Thanks, this is what I have been doing so far (see my last message), but I end up with these conversion issues between types which are just a bit annoying to work with. @Yaël Dillies seemed to suggest that doing set to type coercion was not the way to do this.