mathlibdocumentation

data.set.constructions

Constructions involving sets of sets. #

Finite Intersections #

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

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

finite_inter_closure S is endowed with a term of type has_finite_inter using finite_inter_closure_has_finite_inter.

structure has_finite_inter {α : Type u_1} (S : set (set α)) :
Type
• univ_mem :
• inter_mem : ∀ {s t : set α}, s St Ss t S

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

@[instance]
def has_finite_inter.inhabited {α : Type u_1} :
Equations
inductive has_finite_inter.finite_inter_closure {α : Type u_1} (S : set (set α)) :
set (set α)
• basic : ∀ {α : Type u_1} (S : set (set α)) {s : set α},
• univ : ∀ {α : Type u_1} (S : set (set α)),
• inter : ∀ {α : Type u_1} (S : set (set α)) {s t : set α},

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

Defines has_finite_inter for finite_inter_closure S.

Equations
theorem has_finite_inter.finite_inter_mem {α : Type u_1} {S : set (set α)} (cond : has_finite_inter S) (F : finset (set α)) :
F S⋂₀F S
theorem has_finite_inter.finite_inter_closure_insert {α : Type u_1} {S : set (set α)} {A : set α} (cond : has_finite_inter S) (P : set α) (H : P ) :
P S ∃ (Q : set α) (H : Q S), P = A Q