Constructions involving sets of sets.

Finite Intersections

We define a structure FiniteInter which asserts that a set S of subsets of α is closed under finite intersections.

We define finiteInterClosure which, given a set S of subsets of α, is the smallest set of subsets of α which is closed under finite intersections.

finiteInterClosure S is endowed with a term of type FiniteInter using finiteInterClosure_finiteInter.

structure FiniteInter {α : Type u_1} (S : Set (Set α)) : Prop

A structure encapsulating the fact that a set of sets is closed under finite intersection.

• univ_mem : Set.univ ∈ S

  univ_mem states that Set.univ is in S.

• inter_mem ⦃s : Set α⦄ : s ∈ S → ∀ ⦃t : Set α⦄, t ∈ S → s ∩ t ∈ S

  inter_mem states that any two intersections of sets in S is also in S.

def FiniteInter.finiteInterClosure {α : Type u_1} (S : Set (Set α)) : Set (Set α)

The smallest set of sets containing S which is closed under finite intersections.

Equations

• FiniteInter.finiteInterClosure S = {s : Set α | FiniteInter.MemFiniteInterClosure✝ S s}

@[simp]

theorem FiniteInter.subset_finiteInterClosure {α : Type u_1} (S : Set (Set α)) : S ⊆ finiteInterClosure S

theorem FiniteInter.finiteInterClosure_finiteInter {α : Type u_1} (S : Set (Set α)) : FiniteInter (finiteInterClosure S)

theorem FiniteInter.finiteInterClosure_induction {α : Type u_1} {S : Set (Set α)} {motive : (s : Set α) → s ∈ finiteInterClosure S → Prop} (basic : ∀ (s : Set α) (hs : s ∈ S), motive s ⋯) (univ : motive Set.univ ⋯) (inter : ∀ (s t : Set α) (hs : s ∈ finiteInterClosure S) (ht : t ∈ finiteInterClosure S), motive s hs → motive t ht → motive (s ∩ t) ⋯) {s : Set α} (hs : s ∈ finiteInterClosure S) : motive s hs

An induction principle for membership of finiteInterClosure S. If motive holds of all elements of S and of Set.univ, and is preserved under binary intersections, then it holds of all elements of finiteInterClosure S.

theorem FiniteInter.finiteInterClosure_min {α : Type u_1} {S T : Set (Set α)} (hST : S ⊆ T) (hT : FiniteInter T) : finiteInterClosure S ⊆ T

finiteInterClosure S is the smallest set of sets containing S which is closed under finite intersections.

theorem FiniteInter.finiteInter_mem {α : Type u_1} {S : Set (Set α)} (cond : FiniteInter S) (F : Finset (Set α)) : ↑F ⊆ S → ⋂₀ ↑F ∈ S

theorem FiniteInter.finiteInterClosure_insert {α : Type u_1} {S : Set (Set α)} {A : Set α} (cond : FiniteInter S) (P : Set α) (H : P ∈ finiteInterClosure (insert A S)) : P ∈ S ∨ ∃ Q ∈ S, P = A ∩ Q

theorem FiniteInter.mk₂ {α : Type u_1} {S : Set (Set α)} (h : ∀ ⦃s : Set α⦄, s ∈ S → ∀ ⦃t : Set α⦄, t ∈ S → s ∩ t ∈ S) : FiniteInter (insert Set.univ S)

theorem Set.biUnion_empty_finset {ι : Type u_2} {X : Type u_3} {s : ι → Set X} : ⋃ i ∈ ∅, s i = ∅

This is a hybrid of Set.biUnion_empty and Finset.biUnion_empty (the index set on the LHS is the empty finset, but s is a family of sets, not finsets).