Zulip Chat Archive

Stream: new members

Topic: Powerset of Fintype


Angelo Lucia (Aug 15 2024 at 11:01):

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 (Aug 15 2024 at 11:03):

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 (Aug 15 2024 at 11:24):

or maybe just F and F โІ s?

Yaรซl Dillies (Aug 15 2024 at 11:26):

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

Edward van de Meent (Aug 15 2024 at 11:26):

what second part? :upside_down:

Yaรซl Dillies (Aug 15 2024 at 11:28):

(I was waiting for an answer from Angelo)

Angelo Lucia (Aug 15 2024 at 11:47):

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

Angelo Lucia (Aug 15 2024 at 11:57):

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 (Aug 15 2024 at 12:12):

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 (Aug 15 2024 at 12:18):

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 (Aug 15 2024 at 12:20):

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 (Aug 15 2024 at 12:20):

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

Angelo Lucia (Aug 15 2024 at 12:37):

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 (Aug 15 2024 at 12:43):

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 (Aug 15 2024 at 12:51):

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.


Last updated: May 02 2025 at 03:31 UTC