Constructions involving sets of sets. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source

structure has_finite_inter {α : Type u_1} (S : set (set α)) :

Prop

univ_mem : set.univ ∈ S
inter_mem : ∀ ⦃s : set α⦄, s ∈ S → ∀ ⦃t : set α⦄, t ∈ S → s ∩ t ∈ S

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

source

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

set (set α)

basic : ∀ {α : Type u_1} {S : set (set α)} {s : set α}, s ∈ S → has_finite_inter.finite_inter_closure S s
univ : ∀ {α : Type u_1} {S : set (set α)}, has_finite_inter.finite_inter_closure S set.univ
inter : ∀ {α : Type u_1} {S : set (set α)} {s t : set α}, has_finite_inter.finite_inter_closure S s → has_finite_inter.finite_inter_closure S t → has_finite_inter.finite_inter_closure S (s ∩ t)

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

source

theorem has_finite_inter.finite_inter_closure_has_finite_inter {α : Type u_1} (S : set (set α)) :

has_finite_inter (has_finite_inter.finite_inter_closure S)

source

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

source

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 (has_insert.insert A S)) :

P ∈ S ∨ ∃ (Q : set α) (H : Q ∈ S), P = A ∩ Q