Order the elements of a finset

Stream: Is there code for X?

[Rémy Degenne]

From a Finset S with n elements, I want to get a sequence of n finsets which is increasing for set inclusion and where the finset number k has k elements from S (n+1 finsets starting at the empty finset would also be fine). What is the right way to do that? By right way, I mean the way that gives me the most Mathlib API.

Related question: if I want to impose an order on the elements of a finset and I want to refer to element number k, what is the right way to do that?

I have some old code that did both of those and that I am trying to update, but it feels like the way I did it required way too much new API from me. There are probably some definitions in mathlib that I missed.

[Yaël Dillies]

No, we don't have a way to index elements of a finset. @Yves Jäckle wrote some API for his master project, and @DogaCanSertbas needs some version of that for Schnirelmann's theorem, so I've been basically waiting to see what the use cases are before writing an API.

[Rémy Degenne]

My use case: I have a finset of sets I. Those sets belong to a set semi-ring C docs#MeasureTheory.IsSetSemiring . From that finset of sets, I want to build a finset J of sets in C with the same sUnion, with the added property that all sets in J are pairwise disjoint.
Suppose now that I have I₁ ⊆ I₂ ⊆ ... ⊆ Iₙ = I as described above. Then for all k, by the set semi-ring property, $\bigcup_0 I_k$ can be written as the union of $\bigcup_0 I_{k-1}$ and a finset $J_k$ of pairwise disjoint sets, which are also disjoint with $\bigcup_0 I_{k-1}$. Then the set $J = \bigcup_k J_k$ satisfies all properties I want.

[Yaël Dillies]

The way to do this "disjointification" is docs#disjointed

[Yaël Dillies]

So your finset is not over a linear order?

[Rémy Degenne]

The set difference of two sets in a set semi-ring might not be in the semi-ring, so I have to do more steps to get my disjointed sets.

[Rémy Degenne]

I will try to find a way to replace the ordering by an induction on the size of the finset (I vaguely remember that I failed to do that once, but I might just need to try harder).

[Yaël Dillies]

Oh I see. But the lack of ambient linear order is not necessarily a problem. You can just use an arbitrary total relation.

[Kevin Buzzard]

Doing induction on the size of a finset is slightly mathematically stronger than the usual finset induction property, and I've struggled to do it in the past. There's an ugly hack where you define some intermediate statement P n to be "for all s, s.card = n -> Q s and prove this by induction but I'm sure I've seen some cleverer way

[Ruben Van de Velde]

induction n : s.card generalizing s, maybe? (Untested)

[Yaël Dillies]

Yes, I've done it too, although in Lean 3 so I'm not sure what the corresponding syntax in Lean 4 is.

[Antoine Chambert-Loir]

Starting with docs#Fintype.equivFin, you probably can copy the more or less obvious blackboard definitions. (Is it interesting to cast the result in a more general structure than sets, as a decomposition in docs#Disjoint parts?)