Mathlib.Order.Filter.Bases.Finite

Filter.hasBasis_generate theorem

(s : Set (Set α)) : (generate s).HasBasis (fun t => Set.Finite t ∧ t ⊆ s) fun t => ⋂₀ t

Full source

theorem hasBasis_generate (s : Set (Set α)) :
    (generate s).HasBasis (fun t => Set.FiniteSet.Finite t ∧ t ⊆ s) fun t => ⋂₀ t :=
  ⟨fun U => by simp only [mem_generate_iff, exists_prop, and_assoc, and_left_comm]⟩

Basis Characterization of Generated Filter via Finite Intersections

Informal description

For any collection of sets $s$ on a type $\alpha$, the filter generated by $s$ has a basis consisting of finite intersections of sets from $s$. Specifically, a set $t$ belongs to the generated filter if and only if there exists a finite subset $t' \subseteq s$ such that the intersection $\bigcap t'$ is contained in $t$.

Filter.FilterBasis.ofSets definition

(s : Set (Set α)) : FilterBasis α

Full source

/-- The smallest filter basis containing a given collection of sets. -/
def FilterBasis.ofSets (s : Set (Set α)) : FilterBasis α where
  sets := sIntersInter '' { t | Set.Finite t ∧ t ⊆ s }
  nonempty := ⟨univ, ∅, ⟨⟨finite_empty, empty_subset s⟩, sInter_empty⟩⟩
  inter_sets := by
    rintro _ _ ⟨a, ⟨fina, suba⟩, rfl⟩ ⟨b, ⟨finb, subb⟩, rfl⟩
    exact ⟨⋂₀ (a ∪ b), mem_image_of_mem _ ⟨fina.union finb, union_subset suba subb⟩,
        (sInter_union _ _).subset⟩

Filter basis generated by a collection of sets

Informal description

Given a collection of sets $ s $ over a type $ \alpha $, the function `FilterBasis.ofSets` constructs the smallest filter basis containing $ s $. The sets in this filter basis are precisely the intersections of all finite subsets of $ s $. More formally, the filter basis consists of all sets of the form $ \bigcap₀ t $ where $ t $ is a finite subset of $ s $. The empty intersection is defined to be the universal set, ensuring the basis is nonempty.

Filter.FilterBasis.ofSets_sets theorem

(s : Set (Set α)) : (FilterBasis.ofSets s).sets = sInter '' {t | Set.Finite t ∧ t ⊆ s}

Full source

lemma FilterBasis.ofSets_sets (s : Set (Set α)) :
    (FilterBasis.ofSets s).sets = sIntersInter '' { t | Set.Finite t ∧ t ⊆ s } :=
  rfl

Characterization of Filter Basis Sets via Finite Intersections

Informal description

For any collection of sets $s$ over a type $\alpha$, the sets in the filter basis generated by $s$ are precisely the intersections of all finite subsets of $s$. That is, the collection of sets in the filter basis is equal to the image under $\bigcap₀$ of the collection of all finite subsets $t$ of $s$.

Filter.generate_eq_generate_inter theorem

(s : Set (Set α)) : generate s = generate (sInter '' {t | Set.Finite t ∧ t ⊆ s})

Full source

theorem generate_eq_generate_inter (s : Set (Set α)) :
    generate s = generate (sIntersInter '' { t | Set.Finite t ∧ t ⊆ s }) := by
  rw [← FilterBasis.ofSets_sets, FilterBasis.generate, ← (hasBasis_generate s).filter_eq]; rfl

Equality of Generated Filter and Finite Intersection Generated Filter

Informal description

For any collection of sets $s$ over a type $\alpha$, the filter generated by $s$ is equal to the filter generated by the collection of all finite intersections of sets from $s$. That is, \[ \text{generate } s = \text{generate } \left( \bigcap₀ t \mid t \subseteq s \text{ and } t \text{ is finite} \right). \]

Filter.ofSets_filter_eq_generate theorem

(s : Set (Set α)) : (FilterBasis.ofSets s).filter = generate s

Full source

theorem ofSets_filter_eq_generate (s : Set (Set α)) :
    (FilterBasis.ofSets s).filter = generate s := by
  rw [← (FilterBasis.ofSets s).generate, FilterBasis.ofSets_sets, ← generate_eq_generate_inter]

Equality of Filter Basis Filter and Generated Filter

Informal description

For any collection of sets $s$ over a type $\alpha$, the filter generated by the filter basis constructed from $s$ is equal to the filter generated by $s$ itself. That is, if $B$ is the filter basis consisting of all finite intersections of sets from $s$, then $B.\text{filter} = \text{generate } s$.

Filter.generate_neBot_iff theorem

{s : Set (Set α)} : NeBot (generate s) ↔ ∀ t, t ⊆ s → t.Finite → (⋂₀ t).Nonempty

Full source

theorem generate_neBot_iff {s : Set (Set α)} :
    NeBotNeBot (generate s) ↔ ∀ t, t ⊆ s → t.Finite → (⋂₀ t).Nonempty :=
  (hasBasis_generate s).neBot_iff.trans <| by simp only [← and_imp, and_comm]

Non-triviality Criterion for Generated Filter via Finite Intersections

Informal description

For a collection of sets $s$ on a type $\alpha$, the filter generated by $s$ is non-trivial if and only if every finite subset $t \subseteq s$ has a nonempty intersection, i.e., $\bigcap t \neq \emptyset$.

Filter.hasBasis_iInf' theorem

 {ι : Type*} {ι' : ι → Type*} {l : ι → Filter α} {p : ∀ i, ι' i → Prop} {s : ∀ i, ι' i → Set α}
  (hl : ∀ i, (l i).HasBasis (p i) (s i)) :
  (⨅ i, l i).HasBasis (fun If : Set ι × ∀ i, ι' i => If.1.Finite ∧ ∀ i ∈ If.1, p i (If.2 i))
    fun If : Set ι × ∀ i, ι' i => ⋂ i ∈ If.1, s i (If.2 i)

Full source

theorem hasBasis_iInf' {ι : Type*} {ι' : ι → Type*} {l : ι → Filter α} {p : ∀ i, ι' i → Prop}
    {s : ∀ i, ι' i → Set α} (hl : ∀ i, (l i).HasBasis (p i) (s i)) :
    (⨅ i, l i).HasBasis (fun If : SetSet ι × ∀ i, ι' i => If.1.Finite ∧ ∀ i ∈ If.1, p i (If.2 i))
      fun If : SetSet ι × ∀ i, ι' i => ⋂ i ∈ If.1, s i (If.2 i) :=
  ⟨by
    intro t
    constructor
    · simp only [mem_iInf', (hl _).mem_iff]
      rintro ⟨I, hI, V, hV, -, rfl, -⟩
      choose u hu using hV
      exact ⟨⟨I, u⟩, ⟨hI, fun i _ => (hu i).1⟩, iInter₂_mono fun i _ => (hu i).2⟩
    · rintro ⟨⟨I, f⟩, ⟨hI₁, hI₂⟩, hsub⟩
      refine mem_of_superset ?_ hsub
      exact (biInter_mem hI₁).mpr fun i hi => mem_iInf_of_mem i <| (hl i).mem_of_mem <| hI₂ _ hi⟩

Basis Characterization for Infimum of Filters with Basis

Informal description

Let $\{l_i\}_{i \in \iota}$ be a family of filters on a type $\alpha$, where each filter $l_i$ has a basis consisting of sets $\{s_i(j)\}_{j \in \iota'_i}$ indexed by a predicate $p_i : \iota'_i \to \text{Prop}$. Then the infimum filter $\bigsqcap_i l_i$ has a basis consisting of all finite intersections $\bigcap_{i \in I} s_i(j_i)$, where $I$ is a finite subset of $\iota$ and for each $i \in I$, $j_i \in \iota'_i$ satisfies $p_i(j_i)$.

Filter.hasBasis_iInf theorem

 {ι : Type*} {ι' : ι → Type*} {l : ι → Filter α} {p : ∀ i, ι' i → Prop} {s : ∀ i, ι' i → Set α}
  (hl : ∀ i, (l i).HasBasis (p i) (s i)) :
  (⨅ i, l i).HasBasis (fun If : Σ I : Set ι, ∀ i : I, ι' i => If.1.Finite ∧ ∀ i : If.1, p i (If.2 i)) fun If =>
    ⋂ i : If.1, s i (If.2 i)

Full source

theorem hasBasis_iInf {ι : Type*} {ι' : ι → Type*} {l : ι → Filter α} {p : ∀ i, ι' i → Prop}
    {s : ∀ i, ι' i → Set α} (hl : ∀ i, (l i).HasBasis (p i) (s i)) :
    (⨅ i, l i).HasBasis
      (fun If : Σ I : Set ι, ∀ i : I, ι' i => If.1.Finite ∧ ∀ i : If.1, p i (If.2 i)) fun If =>
      ⋂ i : If.1, s i (If.2 i) := by
  refine ⟨fun t => ⟨fun ht => ?_, ?_⟩⟩
  · rcases (hasBasis_iInf' hl).mem_iff.mp ht with ⟨⟨I, f⟩, ⟨hI, hf⟩, hsub⟩
    exact ⟨⟨I, fun i => f i⟩, ⟨hI, Subtype.forall.mpr hf⟩, trans (iInter_subtype _ _) hsub⟩
  · rintro ⟨⟨I, f⟩, ⟨hI, hf⟩, hsub⟩
    refine mem_of_superset ?_ hsub
    cases hI.nonempty_fintype
    exact iInter_mem.2 fun i => mem_iInf_of_mem ↑i <| (hl i).mem_of_mem <| hf _

Basis characterization for infimum of filters with basis via finite intersections

Informal description

Let $\{l_i\}_{i \in \iota}$ be a family of filters on a type $\alpha$, where each filter $l_i$ has a basis consisting of sets $\{s_i(j)\}_{j \in \iota'_i}$ indexed by a predicate $p_i : \iota'_i \to \text{Prop}$. Then the infimum filter $\bigsqcap_i l_i$ has a basis consisting of all finite intersections $\bigcap_{i \in I} s_i(j_i)$, where $I$ is a finite subset of $\iota$ and for each $i \in I$, $j_i \in \iota'_i$ satisfies $p_i(j_i)$.

Pairwise.exists_mem_filter_basis_of_disjoint theorem

 {I} [Finite I] {l : I → Filter α} {ι : I → Sort*} {p : ∀ i, ι i → Prop} {s : ∀ i, ι i → Set α}
  (hd : Pairwise (Disjoint on l)) (h : ∀ i, (l i).HasBasis (p i) (s i)) :
  ∃ ind : ∀ i, ι i, (∀ i, p i (ind i)) ∧ Pairwise (Disjoint on fun i => s i (ind i))

Full source

theorem _root_.Pairwise.exists_mem_filter_basis_of_disjoint {I} [Finite I] {l : I → Filter α}
    {ι : I → Sort*} {p : ∀ i, ι i → Prop} {s : ∀ i, ι i → Set α} (hd : Pairwise (DisjointDisjoint on l))
    (h : ∀ i, (l i).HasBasis (p i) (s i)) :
    ∃ ind : ∀ i, ι i, (∀ i, p i (ind i)) ∧ Pairwise (Disjoint on fun i => s i (ind i)) := by
  rcases hd.exists_mem_filter_of_disjoint with ⟨t, htl, hd⟩
  choose ind hp ht using fun i => (h i).mem_iff.1 (htl i)
  exact ⟨ind, hp, hd.mono fun i j hij => hij.mono (ht _) (ht _)⟩

Existence of Pairwise Disjoint Basis Sets in Pairwise Disjoint Finite Family of Filters with Basis

Informal description

Let $I$ be a finite index set, and let $(l_i)_{i \in I}$ be a family of filters on a type $\alpha$ such that the filters are pairwise disjoint. Suppose each filter $l_i$ has a basis consisting of sets $(s_i(j))_{j \in \iota_i}$ indexed by a predicate $p_i : \iota_i \to \text{Prop}$. Then there exists a family of indices $(j_i)_{i \in I}$ with $j_i \in \iota_i$ for each $i$, such that: 1. For each $i \in I$, the predicate $p_i(j_i)$ holds. 2. The sets $(s_i(j_i))_{i \in I}$ are pairwise disjoint.

Set.PairwiseDisjoint.exists_mem_filter_basis theorem

 {I : Type*} {l : I → Filter α} {ι : I → Sort*} {p : ∀ i, ι i → Prop} {s : ∀ i, ι i → Set α} {S : Set I}
  (hd : S.PairwiseDisjoint l) (hS : S.Finite) (h : ∀ i, (l i).HasBasis (p i) (s i)) :
  ∃ ind : ∀ i, ι i, (∀ i, p i (ind i)) ∧ S.PairwiseDisjoint fun i => s i (ind i)

Full source

theorem _root_.Set.PairwiseDisjoint.exists_mem_filter_basis {I : Type*} {l : I → Filter α}
    {ι : I → Sort*} {p : ∀ i, ι i → Prop} {s : ∀ i, ι i → Set α} {S : Set I}
    (hd : S.PairwiseDisjoint l) (hS : S.Finite) (h : ∀ i, (l i).HasBasis (p i) (s i)) :
    ∃ ind : ∀ i, ι i, (∀ i, p i (ind i)) ∧ S.PairwiseDisjoint fun i => s i (ind i) := by
  rcases hd.exists_mem_filter hS with ⟨t, htl, hd⟩
  choose ind hp ht using fun i => (h i).mem_iff.1 (htl i)
  exact ⟨ind, hp, hd.mono ht⟩

Existence of Pairwise Disjoint Basis Sets in Finite Pairwise Disjoint Family of Filters with Basis

Informal description

Let $I$ be a type, $(l_i)_{i \in I}$ a family of filters on a type $\alpha$, and $S \subseteq I$ a finite subset. Suppose that for each $i \in I$, the filter $l_i$ has a basis consisting of sets $(s_i(j))_{j \in \iota_i}$ indexed by a predicate $(p_i(j))_{j \in \iota_i}$. If the filters $(l_i)_{i \in S}$ are pairwise disjoint, then there exists an indexed family $(j_i)_{i \in I}$ such that for each $i \in I$, $p_i(j_i)$ holds, and the sets $(s_i(j_i))_{i \in S}$ are pairwise disjoint.

Filter.hasBasis_iInf_principal_finite theorem

{ι : Type*} (s : ι → Set α) : (⨅ i, 𝓟 (s i)).HasBasis (fun t : Set ι => t.Finite) fun t => ⋂ i ∈ t, s i

Full source

/-- If `s : ι → Set α` is an indexed family of sets, then finite intersections of `s i` form a basis
of `⨅ i, 𝓟 (s i)`. -/
theorem hasBasis_iInf_principal_finite {ι : Type*} (s : ι → Set α) :
    (⨅ i, 𝓟 (s i)).HasBasis (fun t : Set ι => t.Finite) fun t => ⋂ i ∈ t, s i := by
  refine ⟨fun U => (mem_iInf_finite _).trans ?_⟩
  simp only [iInf_principal_finset, mem_iUnion, mem_principal, exists_prop,
    exists_finite_iff_finset, Finset.set_biInter_coe]

Finite Intersections Form Basis of Infimum Principal Filters

Informal description

For any indexed family of sets $s : \iota \to \text{Set } \alpha$, the infimum filter $\bigsqcap_i \mathcal{P}(s_i)$ has a basis consisting of finite intersections of the sets $s_i$. Specifically, a set $t$ belongs to $\bigsqcap_i \mathcal{P}(s_i)$ if and only if there exists a finite subset $T \subseteq \iota$ such that $t$ contains the intersection $\bigcap_{i \in T} s_i$.