mathlib documentation

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

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

inductive has_finite_inter.finite_inter_closure {α : Type u_1} (S : set (set α)) :
set (set α)

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

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 has_finite_inter.finite_inter_closure (insert A S)) :
P S ∃ (Q : set α) (H : Q S), P = A Q