Indexed subsets

Stream: general

[Henrik Böving]

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:

$$\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]

@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]

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

[Henrik Böving]

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

[Scott Morrison]

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

[Reid Barton]

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

[Floris van Doorn]

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]

compare docs#is_pi_system

[Henrik Böving]

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

[Eric Wieser]

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]

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

[Yury G. Kudryashov]

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

[Johan Commelin]

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

[Johan Commelin]

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