Documentation

Mathlib.Data.Set.Constructions

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 α)) :

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

Instances For
    theorem FiniteInter.univ_mem {α : Type u_1} {S : Set (Set α)} (self : FiniteInter S) :
    Set.univ S

    univ_mem states that Set.univ is in S.

    theorem FiniteInter.inter_mem {α : Type u_1} {S : Set (Set α)} (self : FiniteInter S) ⦃s : Set α :
    s S∀ ⦃t : Set α⦄, t Ss t S

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

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

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

    Instances For
      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 FiniteInter.finiteInterClosure (insert A S)) :
      P S QS, P = A Q
      theorem FiniteInter.mk₂ {α : Type u_1} {S : Set (Set α)} (h : ∀ ⦃s : Set α⦄, s S∀ ⦃t : Set α⦄, t Ss t S) :
      FiniteInter (insert Set.univ S)