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