Mathlib.Data.Set.Constructions

Module docstring

{"# 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.

FiniteInter structure

Full source

/-- A structure encapsulating the fact that a set of sets is closed under finite intersection. -/
structure FiniteInter : Prop where
  /-- `univ_mem` states that `Set.univ` is in `S`. -/
  univ_mem : Set.univSet.univ ∈ S
  /-- `inter_mem` states that any two intersections of sets in `S` is also in `S`. -/
  inter_mem : ∀ ⦃s⦄, s ∈ S → ∀ ⦃t⦄, t ∈ S → s ∩ ts ∩ t ∈ S

Finite intersection property

Informal description

A structure `FiniteInter` encapsulates the property that a collection $S$ of subsets of a type $\alpha$ is closed under finite intersections, meaning that the intersection of any finite number of sets in $S$ is also in $S$.

FiniteInter.finiteInterClosure inductive

: Set (Set α)

Full source

/-- The smallest set of sets containing `S` which is closed under finite intersections. -/
inductive finiteInterClosure : Set (Set α)
  | basic {s} : s ∈ S → finiteInterClosure s
  | univ : finiteInterClosure Set.univ
  | inter {s t} : finiteInterClosure s → finiteInterClosure t → finiteInterClosure (s ∩ t)

Finite intersection closure of a family of sets

Informal description

The smallest family of subsets of a type $\alpha$ containing a given family $S$ of subsets that is closed under finite intersections. That is, for any finite collection of sets in $\mathrm{finiteInterClosure}\, S$, their intersection is also in $\mathrm{finiteInterClosure}\, S$.

FiniteInter.finiteInterClosure_finiteInter theorem

: FiniteInter (finiteInterClosure S)

Full source

theorem finiteInterClosure_finiteInter : FiniteInter (finiteInterClosure S) :=
  { univ_mem := finiteInterClosure.univ
    inter_mem := fun _ h _ => finiteInterClosure.inter h }

Finite Intersection Property of the Finite Intersection Closure

Informal description

The finite intersection closure $\mathrm{finiteInterClosure}\, S$ of any family $S$ of subsets of a type $\alpha$ satisfies the finite intersection property. That is, for any finite collection of sets in $\mathrm{finiteInterClosure}\, S$, their intersection is also in $\mathrm{finiteInterClosure}\, S$.

FiniteInter.finiteInter_mem theorem

(cond : FiniteInter S) (F : Finset (Set α)) : ↑F ⊆ S → ⋂₀ (↑F : Set (Set α)) ∈ S

Full source

theorem finiteInter_mem (cond : FiniteInter S) (F : Finset (Set α)) :
    ↑F ⊆ S → ⋂₀ (↑F : Set (Set α))⋂₀ (↑F : Set (Set α)) ∈ S := by
  classical
    refine Finset.induction_on F (fun _ => ?_) ?_
    · simp [cond.univ_mem]
    · intro a s _ h1 h2
      suffices a ∩ ⋂₀ ↑sa ∩ ⋂₀ ↑s ∈ S by simpa
      exact
        cond.inter_mem (h2 (Finset.mem_insert_self a s))
          (h1 fun x hx => h2 <| Finset.mem_insert_of_mem hx)

Finite Intersection Property: Membership of Finite Intersections

Informal description

Let $S$ be a collection of subsets of a type $\alpha$ that is closed under finite intersections (i.e., $S$ has the `FiniteInter` property). For any finite set $F$ of subsets of $\alpha$ such that all elements of $F$ are in $S$, the intersection $\bigcap₀ F$ is also in $S$.

FiniteInter.finiteInterClosure_insert theorem

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

Full source

theorem finiteInterClosure_insert {A : Set α} (cond : FiniteInter S) (P)
    (H : P ∈ finiteInterClosure (insert A S)) : P ∈ SP ∈ S ∨ ∃ Q ∈ S, P = A ∩ Q := by
  induction H with
  | basic h =>
    cases h
    · exact Or.inr ⟨Set.univ, cond.univ_mem, by simpa⟩
    · exact Or.inl (by assumption)
  | univ => exact Or.inl cond.univ_mem
  | @inter T1 T2 _ _ h1 h2 =>
    rcases h1 with (h | ⟨Q, hQ, rfl⟩) <;> rcases h2 with (i | ⟨R, hR, rfl⟩)
    · exact Or.inl (cond.inter_mem h i)
    · exact
        Or.inr ⟨T1 ∩ R, cond.inter_mem h hR, by simp only [← Set.inter_assoc, Set.inter_comm _ A]⟩
    · exact Or.inr ⟨Q ∩ T2, cond.inter_mem hQ i, by simp only [Set.inter_assoc]⟩
    · exact
        Or.inr
          ⟨Q ∩ R, cond.inter_mem hQ hR, by
            ext x
            constructor <;> simp +contextual⟩

Characterization of Elements in Finite Intersection Closure with Added Set

Informal description

Let $S$ be a collection of subsets of a type $\alpha$ that is closed under finite intersections. For any subset $A \subseteq \alpha$ and any $P \in \mathrm{finiteInterClosure}(S \cup \{A\})$, either $P \in S$ or there exists $Q \in S$ such that $P = A \cap Q$.

FiniteInter.mk₂ theorem

(h : ∀ ⦃s⦄, s ∈ S → ∀ ⦃t⦄, t ∈ S → s ∩ t ∈ S) : FiniteInter (insert (univ : Set α) S)

Full source

theorem mk₂ (h : ∀ ⦃s⦄, s ∈ S → ∀ ⦃t⦄, t ∈ S → s ∩ ts ∩ t ∈ S) :
    FiniteInter (insert (univ : Set α) S) where
  univ_mem := Set.mem_insert Set.univ S
  inter_mem s hs t ht := by aesop

Finite Intersection Property for Extended Collection with Universal Set

Informal description

Given a collection $S$ of subsets of a type $\alpha$, if for any two sets $s, t \in S$ their intersection $s \cap t$ is also in $S$, then the collection obtained by inserting the universal set $\text{univ} \subseteq \alpha$ into $S$ has the finite intersection property.