Set Systems?

Stream: Is there code for X?

[Jihoon Hyun]

Hello, is there a definition of set systems, a tuple of a ground set E and the subset of the power set of E, and some of its properties such as accessibility?

[Martin Dvořák]

I think so. The paper "Formalizing Hall’s Marriage Theorem in Lean" works with that and it became a part of mathlib.

[Martin Dvořák]

Actually they used indexed families of sets:
https://github.com/leanprover-community/mathlib/blob/1e6b748c175e64dd033d7a1a1bfe3e9fe72011d3/src/combinatorics/hall/finite.lean#L260

[Martin Dvořák]

They have t : ι → finset E whereι is a finite type.

[Martin Dvořák]

They don't have "set system" as a structure.

[Martin Dvořák]

Jihoon Hyun said:

Hello, is there a definition of set systems, a tuple of a ground set E and the subset of the power set of E, and some of its properties such as accessibility?

Do you want to enforce that each subset of E exists at most once in the set system?

[Yaël Dillies]

What's your use? If you want to do combinatorics, your best bet is finset (finset E) and you can find a bunch of examples in the folder combinatorics/set_family.

[Yaël Dillies]

There are also set systems in topology and measure theory in the form of docs#topological_space, docs#measure_theory.measurable_space, docs#measure_theory.d_system.

[Martin Dvořák]

Yaël Dillies said:

There are also set systems in topology and measure theory in the form of docs#topological_space, docs#measure_theory.measurable_space, docs#measure_theory.d_system.

The first link works.

[Yaël Dillies]

Sorry, I never remember what's in the measure_theory namespace and what's not :sweat_smile:

[Jihoon Hyun]

Yaël Dillies 말함:

What's your use? If you want to do combinatorics, your best bet is finset (finset E) and you can find a bunch of examples in the folder combinatorics/set_family.

As I'm trying to use it with combinatorics, this seems like a reasonable approach. I'd like to make use of several finite -oid structures, should I assume implementations of such structures does not exist?

[Yaël Dillies]

Indeed, they don't exist because we don't need them. What theorem are you trying to prove?

[Jihoon Hyun]

I have no theorem in mind yet, it just was odd to me there were no implementation of those. I'm a lean4 user, what should I do to contribute to, for example mathlib4?

[Martin Dvořák]

FYI, the paper I mentioned uses Lean 3.

[Yaël Dillies]

Without docs#finset being ported to mathlib4, you will have a hard time doing anything.

[Yaël Dillies]

If you want to do combinatorics, I strongly suggest you stick to Lean 3 for the time being.

[Martin Dvořák]

Is it because combinatorics is at the end of the food chain?

[Yaël Dillies]

No, not quite. Set family combinatorics has quite low imports, but when you get to stuff like Behrend's bound (docs#behrend.roth_lower_bound) it suddenly pulls in a lot of analysis.