Zulip Chat Archive

Stream: general

Topic: Indexed subsets


Henrik Böving (Oct 11 2021 at 10:42):

I'm doing some set theory and stumbled upon something I am rather unsure how to express in Lean, basically if A : set (set α) I'd like to express something like:

A1,A2,,AnA,(i=0nAi)A\forall A_1, A_2, \dots, A_n \in A, \left(\bigcup_{i=0}^n A_i \right) \in A

And I have no idea at all how to deal with these indexed subsets of A, would someone happen to know?

Johan Commelin (Oct 11 2021 at 10:47):

@Henrik Böving There are basically two options: you can work with an (unordered) set of sets: As : set (set X). Or you can have a function I → set X, where I is an indexing type such as fin n.

Johan Commelin (Oct 11 2021 at 10:47):

In the second case, I could or could not come with an ordering.

Henrik Böving (Oct 11 2021 at 11:12):

Would there be any advantages from one over the other in this specific case?

Scott Morrison (Oct 11 2021 at 11:24):

I might use ∀ X : finset A, and using finset.sup to express the condition you want.

Reid Barton (Oct 11 2021 at 11:36):

Depending on the situation you might also get by with just the cases n = 2 and (if applicable) n = 0

Floris van Doorn (Oct 11 2021 at 11:40):

Here are some ways to express this. I recommend going with Reid's suggestion (option 4)

import data.finset.lattice
import data.set.finite

variables {α : Type*}
def closed_under_finite_unions1 (A : set (set α)) : Prop :=
 B : finset (set α), B  A  B.sup id  A

def closed_under_finite_unions2 (A : set (set α)) : Prop :=
 B : set (set α), B.finite  B  A  ⋃₀ B  A

def {u} closed_under_finite_unions3 {α : Type u} (A : set (set α)) : Prop :=
 (ι : Type u) (B : ι  set α), fintype ι  ( i, B i  A)  ( i, B i)  A

def closed_under_finite_unions4 (A : set (set α)) : Prop :=
  A   A₁ A₂  A, A₁  A₂  A

You can then have the other versions as theorems.

Floris van Doorn (Oct 11 2021 at 11:41):

compare docs#is_pi_system

Henrik Böving (Oct 11 2021 at 11:52):

I went with the indexed approach for now since it most closely matches what I want to express, thanks to everyone!

Eric Wieser (Oct 11 2021 at 12:05):

It's worth noting that you can always recover the set version from the indexed version by choosing I as coe_sort As and f : I → set X as coe

Yury G. Kudryashov (Oct 11 2021 at 14:52):

It may be convenient to require closed_under_finite_unions4 in the definition, then have others as theorems.

Yury G. Kudryashov (Oct 11 2021 at 14:53):

Because it will be easier to prove that some set of sets satisfies the predicate.

Johan Commelin (Oct 11 2021 at 14:54):

Also, in version 3 the ι is restricted to universe u. In a lemma you could remove that restriction.

Johan Commelin (Oct 11 2021 at 14:54):

(You'll certainly be happy to have the flexibility to use ι = fin n)


Last updated: Dec 20 2023 at 11:08 UTC