doc-next-gen

Mathlib.Order.Filter.Finite

Module docstring

{"# Results filters related to finiteness.

","### Lattice equations ","#### principal equations ","### Eventually ","### Relation “eventually equal” "}

Filter.biInter_mem theorem
{β : Type v} {s : β → Set α} {is : Set β} (hf : is.Finite) : (⋂ i ∈ is, s i) ∈ f ↔ ∀ i ∈ is, s i ∈ f
Full source 
@[simp]
theorem biInter_mem {β : Type v} {s : β → Set α} {is : Set β} (hf : is.Finite) :
    (⋂ i ∈ is, s i) ∈ f(⋂ i ∈ is, s i) ∈ f ↔ ∀ i ∈ is, s i ∈ f := by
  induction is, hf using Set.Finite.induction_on with
  | empty => simp
  | insert _ _ hs => simp [hs]
Finite Intersection Property for Filters
Informal description
Let $f$ be a filter on a type $\alpha$, $\beta$ be a type, $s : \beta \to \text{Set } \alpha$ be a family of sets, and $is \subseteq \beta$ be a finite subset. Then the intersection $\bigcap_{i \in is} s(i)$ belongs to $f$ if and only if for every $i \in is$, the set $s(i)$ belongs to $f$.
Filter.biInter_finset_mem theorem
{β : Type v} {s : β → Set α} (is : Finset β) : (⋂ i ∈ is, s i) ∈ f ↔ ∀ i ∈ is, s i ∈ f
Full source 
@[simp]
theorem biInter_finset_mem {β : Type v} {s : β → Set α} (is : Finset β) :
    (⋂ i ∈ is, s i) ∈ f(⋂ i ∈ is, s i) ∈ f ↔ ∀ i ∈ is, s i ∈ f :=
  biInter_mem is.finite_toSet
Finite Intersection Property for Filters with Finset Indices
Informal description
Let $f$ be a filter on a type $\alpha$, $\beta$ be a type, $s : \beta \to \text{Set } \alpha$ be a family of sets, and $is$ be a finite set of indices of type $\beta$. Then the intersection $\bigcap_{i \in is} s(i)$ belongs to $f$ if and only if for every $i \in is$, the set $s(i)$ belongs to $f$.
Filter.sInter_mem theorem
{s : Set (Set α)} (hfin : s.Finite) : ⋂₀ s ∈ f ↔ ∀ U ∈ s, U ∈ f
Full source 
@[simp]
theorem sInter_mem {s : Set (Set α)} (hfin : s.Finite) : ⋂₀ s⋂₀ s ∈ f⋂₀ s ∈ f ↔ ∀ U ∈ s, U ∈ f := by
  rw [sInter_eq_biInter, biInter_mem hfin]
Finite Intersection Property for Filters with Set Collection
Informal description
Let $f$ be a filter on a type $\alpha$ and $s$ be a finite collection of subsets of $\alpha$. Then the intersection $\bigcap s$ belongs to $f$ if and only if every subset $U \in s$ belongs to $f$.
Filter.iInter_mem theorem
{β : Sort v} {s : β → Set α} [Finite β] : (⋂ i, s i) ∈ f ↔ ∀ i, s i ∈ f
Full source 
@[simp]
theorem iInter_mem {β : Sort v} {s : β → Set α} [Finite β] : (⋂ i, s i) ∈ f(⋂ i, s i) ∈ f ↔ ∀ i, s i ∈ f :=
  (sInter_mem (finite_range _)).trans forall_mem_range
Finite Intersection Property for Filters with Finite Index Type
Informal description
Let $f$ be a filter on a type $\alpha$, $\beta$ be a finite type, and $s : \beta \to \text{Set } \alpha$ be a family of sets. Then the intersection $\bigcap_{i \in \beta} s(i)$ belongs to $f$ if and only if for every $i \in \beta$, the set $s(i)$ belongs to $f$.
Filter.mem_generate_iff theorem
{s : Set <| Set α} {U : Set α} : U ∈ generate s ↔ ∃ t ⊆ s, Set.Finite t ∧ ⋂₀ t ⊆ U
Full source 
theorem mem_generate_iff {s : Set <| Set α} {U : Set α} :
    U ∈ generate sU ∈ generate s ↔ ∃ t ⊆ s, Set.Finite t ∧ ⋂₀ t ⊆ U := by
  constructor <;> intro h
  · induction h with
    | @basic V V_in =>
      exact ⟨{V}, singleton_subset_iff.2 V_in, finite_singleton _, (sInter_singleton _).subset⟩
    | univ => exact ⟨∅, empty_subset _, finite_empty, subset_univ _⟩
    | superset _ hVW hV =>
      rcases hV with ⟨t, hts, ht, htV⟩
      exact ⟨t, hts, ht, htV.trans hVW⟩
    | inter _ _ hV hW =>
      rcases hV, hW with ⟨⟨t, hts, ht, htV⟩, u, hus, hu, huW⟩
      exact
        ⟨t ∪ u, union_subset hts hus, ht.union hu,
          (sInter_union _ _).subset.trans <| inter_subset_inter htV huW⟩
  · rcases h with ⟨t, hts, tfin, h⟩
    exact mem_of_superset ((sInter_mem tfin).2 fun V hV => GenerateSets.basic <| hts hV) h
Characterization of Filter Generation via Finite Subcollections
Informal description
Let $s$ be a collection of subsets of a type $\alpha$ and $U$ be a subset of $\alpha$. Then $U$ belongs to the filter generated by $s$ if and only if there exists a finite subset $t \subseteq s$ such that the intersection $\bigcap t$ is contained in $U$.
Filter.mem_iInf_of_iInter theorem
{ι} {s : ι → Filter α} {U : Set α} {I : Set ι} (I_fin : I.Finite) {V : I → Set α} (hV : ∀ (i : I), V i ∈ s i) (hU : ⋂ i, V i ⊆ U) : U ∈ ⨅ i, s i
Full source 
theorem mem_iInf_of_iInter {ι} {s : ι → Filter α} {U : Set α} {I : Set ι} (I_fin : I.Finite)
    {V : I → Set α} (hV : ∀ (i : I), V i ∈ s i) (hU : ⋂ i, V i⋂ i, V i ⊆ U) : U ∈ ⨅ i, s i := by
  haveI := I_fin.fintype
  refine mem_of_superset (iInter_mem.2 fun i => ?_) hU
  exact mem_iInf_of_mem (i : ι) (hV _)
Membership in Infimum Filter via Finite Intersection
Informal description
Let $\{s_i\}_{i \in \iota}$ be a family of filters on a type $\alpha$, $U$ be a subset of $\alpha$, and $I$ be a finite subset of $\iota$. Suppose for each $i \in I$, there exists a set $V_i \in s_i$ such that the intersection $\bigcap_{i \in I} V_i$ is contained in $U$. Then $U$ belongs to the infimum filter $\bigsqcap_{i \in \iota} s_i$.
Filter.mem_iInf theorem
{ι} {s : ι → Filter α} {U : Set α} : (U ∈ ⨅ i, s i) ↔ ∃ I : Set ι, I.Finite ∧ ∃ V : I → Set α, (∀ (i : I), V i ∈ s i) ∧ U = ⋂ i, V i
Full source 
theorem mem_iInf {ι} {s : ι → Filter α} {U : Set α} :
    (U ∈ ⨅ i, s i) ↔
      ∃ I : Set ι, I.Finite ∧ ∃ V : I → Set α, (∀ (i : I), V i ∈ s i) ∧ U = ⋂ i, V i := by
  constructor
  · rw [iInf_eq_generate, mem_generate_iff]
    rintro ⟨t, tsub, tfin, tinter⟩
    rcases eq_finite_iUnion_of_finite_subset_iUnion tfin tsub with ⟨I, Ifin, σ, σfin, σsub, rfl⟩
    rw [sInter_iUnion] at tinter
    set V := fun i => U ∪ ⋂₀ σ i with hV
    have V_in : ∀ (i : I), V i ∈ s i := by
      rintro i
      have : ⋂₀ σ i⋂₀ σ i ∈ s i := by
        rw [sInter_mem (σfin _)]
        apply σsub
      exact mem_of_superset this subset_union_right
    refine ⟨I, Ifin, V, V_in, ?_⟩
    rwa [hV, ← union_iInter, union_eq_self_of_subset_right]
  · rintro ⟨I, Ifin, V, V_in, rfl⟩
    exact mem_iInf_of_iInter Ifin V_in Subset.rfl
Characterization of Membership in Infimum Filter via Finite Intersection
Informal description
Let $\{s_i\}_{i \in \iota}$ be a family of filters on a type $\alpha$ and $U$ be a subset of $\alpha$. Then $U$ belongs to the infimum filter $\bigsqcap_i s_i$ if and only if there exists a finite subset $I \subseteq \iota$ and a family of sets $\{V_i\}_{i \in I}$ such that: - For each $i \in I$, $V_i \in s_i$. - $U = \bigcap_{i \in I} V_i$.
Filter.mem_iInf' theorem
{ι} {s : ι → Filter α} {U : Set α} : (U ∈ ⨅ i, s i) ↔ ∃ I : Set ι, I.Finite ∧ ∃ V : ι → Set α, (∀ i, V i ∈ s i) ∧ (∀ i ∉ I, V i = univ) ∧ (U = ⋂ i ∈ I, V i) ∧ U = ⋂ i, V i
Full source 
theorem mem_iInf' {ι} {s : ι → Filter α} {U : Set α} :
    (U ∈ ⨅ i, s i) ↔
      ∃ I : Set ι, I.Finite ∧ ∃ V : ι → Set α, (∀ i, V i ∈ s i) ∧
        (∀ i ∉ I, V i = univ) ∧ (U = ⋂ i ∈ I, V i) ∧ U = ⋂ i, V i := by
  classical
  simp only [mem_iInf, SetCoe.forall', biInter_eq_iInter]
  refine ⟨?_, fun ⟨I, If, V, hVs, _, hVU, _⟩ => ⟨I, If, fun i => V i, fun i => hVs i, hVU⟩⟩
  rintro ⟨I, If, V, hV, rfl⟩
  refine ⟨I, If, fun i => if hi : i ∈ I then V ⟨i, hi⟩ else univ, fun i => ?_, fun i hi => ?_, ?_⟩
  · dsimp only
    split_ifs
    exacts [hV ⟨i,_⟩, univ_mem]
  · exact dif_neg hi
  · simp only [iInter_dite, biInter_eq_iInter, dif_pos (Subtype.coe_prop _), Subtype.coe_eta,
      iInter_univ, inter_univ, eq_self_iff_true, true_and]
Characterization of Membership in Infimum of Filters via Finite Subfamily
Informal description
For a family of filters $\{s_i\}_{i \in \iota}$ on a type $\alpha$ and a set $U \subseteq \alpha$, the following are equivalent: 1. $U$ belongs to the infimum filter $\bigsqcap_i s_i$. 2. There exists a finite subset $I \subseteq \iota$ and a family of sets $\{V_i\}_{i \in \iota}$ such that: - For each $i \in \iota$, $V_i \in s_i$. - For each $i \notin I$, $V_i = \text{univ}$ (the universal set). - $U = \bigcap_{i \in I} V_i$ and $U = \bigcap_i V_i$.
Filter.exists_iInter_of_mem_iInf theorem
{ι : Sort*} {α : Type*} {f : ι → Filter α} {s} (hs : s ∈ ⨅ i, f i) : ∃ t : ι → Set α, (∀ i, t i ∈ f i) ∧ s = ⋂ i, t i
Full source 
theorem exists_iInter_of_mem_iInf {ι : Sort*} {α : Type*} {f : ι → Filter α} {s}
    (hs : s ∈ ⨅ i, f i) : ∃ t : ι → Set α, (∀ i, t i ∈ f i) ∧ s = ⋂ i, t i := by
  rw [← iInf_range' (g := (·))] at hs
  let ⟨_, _, V, hVs, _, _, hVU'⟩ := mem_iInf'.1 hs
  use V ∘ rangeFactorization f, fun i ↦ hVs (rangeFactorization f i)
  rw [hVU', ← surjective_onto_range.iInter_comp, comp_def]
Existence of Intersection Family for Infimum Filter Membership
Informal description
For any family of filters $\{f_i\}_{i \in \iota}$ on a type $\alpha$ and any set $s \subseteq \alpha$, if $s$ belongs to the infimum filter $\bigsqcap_i f_i$, then there exists a family of sets $\{t_i\}_{i \in \iota}$ such that: - For each $i \in \iota$, $t_i \in f_i$. - $s = \bigcap_{i \in \iota} t_i$.
Filter.mem_iInf_of_finite theorem
{ι : Sort*} [Finite ι] {α : Type*} {f : ι → Filter α} (s) : (s ∈ ⨅ i, f i) ↔ ∃ t : ι → Set α, (∀ i, t i ∈ f i) ∧ s = ⋂ i, t i
Full source 
theorem mem_iInf_of_finite {ι : Sort*} [Finite ι] {α : Type*} {f : ι → Filter α} (s) :
    (s ∈ ⨅ i, f i) ↔ ∃ t : ι → Set α, (∀ i, t i ∈ f i) ∧ s = ⋂ i, t i := by
  refine ⟨exists_iInter_of_mem_iInf, ?_⟩
  rintro ⟨t, ht, rfl⟩
  exact iInter_mem.2 fun i => mem_iInf_of_mem i (ht i)
Finite Infimum Filter Membership Characterization via Intersections
Informal description
For a finite index type $\iota$, a family of filters $\{f_i\}_{i \in \iota}$ on a type $\alpha$, and a set $s \subseteq \alpha$, the following are equivalent: 1. $s$ belongs to the infimum filter $\bigsqcap_i f_i$. 2. There exists a family of sets $\{t_i\}_{i \in \iota}$ such that for each $i \in \iota$, $t_i \in f_i$, and $s = \bigcap_{i \in \iota} t_i$.
Filter.mem_biInf_principal theorem
{ι : Type*} {p : ι → Prop} {s : ι → Set α} {t : Set α} : t ∈ ⨅ (i : ι) (_ : p i), 𝓟 (s i) ↔ ∃ I : Set ι, I.Finite ∧ (∀ i ∈ I, p i) ∧ ⋂ i ∈ I, s i ⊆ t
Full source 
theorem mem_biInf_principal {ι : Type*} {p : ι → Prop} {s : ι → Set α} {t : Set α} :
    t ∈ ⨅ (i : ι) (_ : p i), 𝓟 (s i)t ∈ ⨅ (i : ι) (_ : p i), 𝓟 (s i) ↔
      ∃ I : Set ι, I.Finite ∧ (∀ i ∈ I, p i) ∧ ⋂ i ∈ I, s i ⊆ t := by
  constructor
  · simp only [mem_iInf (ι := ι), mem_iInf_of_finite, mem_principal]
    rintro ⟨I, hIf, V, hV₁, hV₂, rfl⟩
    choose! t ht₁ ht₂ using hV₁
    refine ⟨I ∩ {i | p i}, hIf.inter_of_left _, fun i ↦ And.right, ?_⟩
    simp only [mem_inter_iff, iInter_and, biInter_eq_iInter, ht₂, mem_setOf_eq]
    gcongr with i hpi
    exact ht₁ i hpi
  · rintro ⟨I, hIf, hpI, hst⟩
    rw [biInter_eq_iInter] at hst
    refine mem_iInf_of_iInter hIf (fun i ↦ ?_) hst
    simp [hpI i i.2]
Characterization of Membership in Infimum of Principal Filters via Finite Intersection
Informal description
Let $\iota$ be a type, $p : \iota \to \mathrm{Prop}$ a predicate on $\iota$, $\{s_i\}_{i \in \iota}$ a family of subsets of a type $\alpha$, and $t \subseteq \alpha$. Then $t$ belongs to the infimum filter $\bigsqcap_{i \in \iota, p(i)} \mathrm{principal}(s_i)$ if and only if there exists a finite subset $I \subseteq \iota$ such that: 1. For all $i \in I$, $p(i)$ holds. 2. The intersection $\bigcap_{i \in I} s_i$ is contained in $t$.
Pairwise.exists_mem_filter_of_disjoint theorem
{ι : Type*} [Finite ι] {l : ι → Filter α} (hd : Pairwise (Disjoint on l)) : ∃ s : ι → Set α, (∀ i, s i ∈ l i) ∧ Pairwise (Disjoint on s)
Full source 
theorem _root_.Pairwise.exists_mem_filter_of_disjoint {ι : Type*} [Finite ι] {l : ι → Filter α}
    (hd : Pairwise (DisjointDisjoint on l)) :
    ∃ s : ι → Set α, (∀ i, s i ∈ l i) ∧ Pairwise (Disjoint on s) := by
  have : Pairwise fun i j => ∃ (s : {s // s ∈ l i}) (t : {t // t ∈ l j}), Disjoint s.1 t.1 := by
    simpa only [Pairwise, Function.onFun, Filter.disjoint_iff, exists_prop, Subtype.exists] using hd
  choose! s t hst using this
  refine ⟨fun i => ⋂ j, @s i j ∩ @t j i, fun i => ?_, fun i j hij => ?_⟩
  exacts [iInter_mem.2 fun j => inter_mem (@s i j).2 (@t j i).2,
    (hst hij).mono ((iInter_subset _ j).trans inter_subset_left)
      ((iInter_subset _ i).trans inter_subset_right)]
Existence of Pairwise Disjoint Sets in Pairwise Disjoint Finite Family of Filters
Informal description
Let $\iota$ be a finite type and $(l_i)_{i \in \iota}$ be a family of filters on a type $\alpha$ such that the filters are pairwise disjoint. Then there exists a family of sets $(s_i)_{i \in \iota}$ where each $s_i$ belongs to the filter $l_i$, and the sets $s_i$ are pairwise disjoint.
Set.PairwiseDisjoint.exists_mem_filter theorem
{ι : Type*} {l : ι → Filter α} {t : Set ι} (hd : t.PairwiseDisjoint l) (ht : t.Finite) : ∃ s : ι → Set α, (∀ i, s i ∈ l i) ∧ t.PairwiseDisjoint s
Full source 
theorem _root_.Set.PairwiseDisjoint.exists_mem_filter {ι : Type*} {l : ι → Filter α} {t : Set ι}
    (hd : t.PairwiseDisjoint l) (ht : t.Finite) :
    ∃ s : ι → Set α, (∀ i, s i ∈ l i) ∧ t.PairwiseDisjoint s := by
  haveI := ht.to_subtype
  rcases (hd.subtype _ _).exists_mem_filter_of_disjoint with ⟨s, hsl, hsd⟩
  lift s to (i : t) → {s // s ∈ l i} using hsl
  rcases @Subtype.exists_pi_extension ι (fun i => { s // s ∈ l i }) _ _ s with ⟨s, rfl⟩
  exact ⟨fun i => s i, fun i => (s i).2, hsd.set_of_subtype _ _⟩
Existence of Pairwise Disjoint Sets in Finite Pairwise Disjoint Family of Filters
Informal description
Let $\iota$ be a type, $(l_i)_{i \in \iota}$ a family of filters on a type $\alpha$, and $t \subseteq \iota$ a finite subset. If the filters $(l_i)_{i \in t}$ are pairwise disjoint, then there exists a family of sets $(s_i)_{i \in \iota}$ such that each $s_i$ belongs to $l_i$ and the sets $(s_i)_{i \in t}$ are pairwise disjoint.
Filter.iInf_sets_eq_finite theorem
{ι : Type*} (f : ι → Filter α) : (⨅ i, f i).sets = ⋃ t : Finset ι, (⨅ i ∈ t, f i).sets
Full source 
theorem iInf_sets_eq_finite {ι : Type*} (f : ι → Filter α) :
    (⨅ i, f i).sets = ⋃ t : Finset ι, (⨅ i ∈ t, f i).sets := by
  rw [iInf_eq_iInf_finset, iInf_sets_eq]
  exact directed_of_isDirected_le fun _ _ => biInf_mono
Characterization of Infimum Filter Sets via Finite Subsets
Informal description
For any family of filters $(f_i)_{i \in \iota}$ on a type $\alpha$, the collection of sets in the infimum filter $\bigsqcap_i f_i$ is equal to the union over all finite subsets $t \subseteq \iota$ of the sets in the finite infimum filter $\bigsqcap_{i \in t} f_i$. In other words, a set $s$ belongs to $\bigsqcap_i f_i$ if and only if there exists a finite subset $t \subseteq \iota$ such that $s$ belongs to $\bigsqcap_{i \in t} f_i$.
Filter.iInf_sets_eq_finite' theorem
(f : ι → Filter α) : (⨅ i, f i).sets = ⋃ t : Finset (PLift ι), (⨅ i ∈ t, f (PLift.down i)).sets
Full source 
theorem iInf_sets_eq_finite' (f : ι → Filter α) :
    (⨅ i, f i).sets = ⋃ t : Finset (PLift ι), (⨅ i ∈ t, f (PLift.down i)).sets := by
  rw [← iInf_sets_eq_finite, ← Equiv.plift.surjective.iInf_comp, Equiv.plift_apply]
Characterization of Infimum Filter Sets via Finite Subsets (PLift Version)
Informal description
For any family of filters $(f_i)_{i \in \iota}$ on a type $\alpha$, the collection of sets in the infimum filter $\bigsqcap_i f_i$ is equal to the union over all finite subsets $t \subseteq \iota$ (represented as `Finset (PLift ι)`) of the sets in the finite infimum filter $\bigsqcap_{i \in t} f_i$. In other words, a set $s$ belongs to $\bigsqcap_i f_i$ if and only if there exists a finite subset $t \subseteq \iota$ (via the `PLift` representation) such that $s$ belongs to $\bigsqcap_{i \in t} f_i$.
Filter.mem_iInf_finite theorem
{ι : Type*} {f : ι → Filter α} (s) : s ∈ iInf f ↔ ∃ t : Finset ι, s ∈ ⨅ i ∈ t, f i
Full source 
theorem mem_iInf_finite {ι : Type*} {f : ι → Filter α} (s) :
    s ∈ iInf fs ∈ iInf f ↔ ∃ t : Finset ι, s ∈ ⨅ i ∈ t, f i :=
  (Set.ext_iff.1 (iInf_sets_eq_finite f) s).trans mem_iUnion
Membership in Infimum Filter via Finite Subsets
Informal description
For any family of filters $(f_i)_{i \in \iota}$ on a type $\alpha$ and any set $s$, $s$ belongs to the infimum filter $\bigsqcap_i f_i$ if and only if there exists a finite subset $t \subseteq \iota$ such that $s$ belongs to the finite infimum filter $\bigsqcap_{i \in t} f_i$.
Filter.mem_iInf_finite' theorem
{f : ι → Filter α} (s) : s ∈ iInf f ↔ ∃ t : Finset (PLift ι), s ∈ ⨅ i ∈ t, f (PLift.down i)
Full source 
theorem mem_iInf_finite' {f : ι → Filter α} (s) :
    s ∈ iInf fs ∈ iInf f ↔ ∃ t : Finset (PLift ι), s ∈ ⨅ i ∈ t, f (PLift.down i) :=
  (Set.ext_iff.1 (iInf_sets_eq_finite' f) s).trans mem_iUnion
Membership in Infimum Filter via Finite Subsets (Lifted Indices Version)
Informal description
For a family of filters $(f_i)_{i \in \iota}$ on a type $\alpha$ and a set $s$, $s$ belongs to the infimum filter $\bigsqcap_i f_i$ if and only if there exists a finite subset $t \subseteq \iota$ (represented as a finite set of lifted indices via `PLift`) such that $s$ belongs to the finite infimum filter $\bigsqcap_{i \in t} f_i$.
Filter.coframeMinimalAxioms abbrev
: Coframe.MinimalAxioms (Filter α)
Full source 
/-- The dual version does not hold! `Filter α` is not a `CompleteDistribLattice`. -/
-- See note [reducible non-instances]
abbrev coframeMinimalAxioms : Coframe.MinimalAxioms (Filter α) :=
  { Filter.instCompleteLatticeFilter with
    iInf_sup_le_sup_sInf := fun f s t ⟨h₁, h₂⟩ => by
      classical
      rw [iInf_subtype']
      rw [sInf_eq_iInf', ← Filter.mem_sets, iInf_sets_eq_finite, mem_iUnion] at h₂
      obtain ⟨u, hu⟩ := h₂
      rw [← Finset.inf_eq_iInf] at hu
      suffices ⨅ i : s, f ⊔ ↑i ≤ f ⊔ u.inf fun i => ↑i from this ⟨h₁, hu⟩
      refine Finset.induction_on u (le_sup_of_le_right le_top) ?_
      rintro ⟨i⟩ u _ ih
      rw [Finset.inf_insert, sup_inf_left]
      exact le_inf (iInf_le _ _) ih }
Filter Type Satisfies Coframe Minimal Axioms
Informal description
The filter type `Filter α` satisfies the minimal axioms of a coframe structure.
Filter.instCoframe instance
: Coframe (Filter α)
Full source 
instance instCoframe : Coframe (Filter α) := .ofMinimalAxioms coframeMinimalAxioms
Filters Form a Coframe
Informal description
For any type $\alpha$, the lattice of filters on $\alpha$ forms a coframe. That is, it is a complete lattice satisfying the coframe distributivity condition: for any filter $f$ and any family of filters $(g_i)_{i \in I}$, we have $f \sqcup \bigsqcap_{i \in I} g_i = \bigsqcap_{i \in I} (f \sqcup g_i)$.
Filter.mem_iInf_finset theorem
{s : Finset α} {f : α → Filter β} {t : Set β} : (t ∈ ⨅ a ∈ s, f a) ↔ ∃ p : α → Set β, (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ a ∈ s, p a
Full source 
theorem mem_iInf_finset {s : Finset α} {f : α → Filter β} {t : Set β} :
    (t ∈ ⨅ a ∈ s, f a) ↔ ∃ p : α → Set β, (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ a ∈ s, p a := by
  classical
  simp only [← Finset.set_biInter_coe, biInter_eq_iInter, iInf_subtype']
  refine ⟨fun h => ?_, ?_⟩
  · rcases (mem_iInf_of_finite _).1 h with ⟨p, hp, rfl⟩
    refine ⟨fun a => if h : a ∈ s then p ⟨a, h⟩ else univ,
            fun a ha => by simpa [ha] using hp ⟨a, ha⟩, ?_⟩
    refine iInter_congr_of_surjective id surjective_id ?_
    rintro ⟨a, ha⟩
    simp [ha]
  · rintro ⟨p, hpf, rfl⟩
    exact iInter_mem.2 fun a => mem_iInf_of_mem a (hpf a a.2)
Finite Infimum Filter Membership via Intersection Representation
Informal description
For a finite set $s \subseteq \alpha$, a family of filters $\{f_a\}_{a \in \alpha}$ on a type $\beta$, and a set $t \subseteq \beta$, the following are equivalent: 1. $t$ belongs to the infimum filter $\bigsqcap_{a \in s} f_a$. 2. There exists a family of sets $\{p_a\}_{a \in \alpha}$ such that for each $a \in s$, $p_a \in f_a$, and $t = \bigcap_{a \in s} p_a$.
Filter.iInf_sets_induct theorem
{f : ι → Filter α} {s : Set α} (hs : s ∈ iInf f) {p : Set α → Prop} (uni : p univ) (ins : ∀ {i s₁ s₂}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)) : p s
Full source 
@[elab_as_elim]
theorem iInf_sets_induct {f : ι → Filter α} {s : Set α} (hs : s ∈ iInf f) {p : Set α → Prop}
    (uni : p univ) (ins : ∀ {i s₁ s₂}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)) : p s := by
  classical
  rw [mem_iInf_finite'] at hs
  simp only [← Finset.inf_eq_iInf] at hs
  rcases hs with ⟨is, his⟩
  induction is using Finset.induction_on generalizing s with
  | empty => rwa [mem_top.1 his]
  | insert _ _ _ ih =>
    rw [Finset.inf_insert, mem_inf_iff] at his
    rcases his with ⟨s₁, hs₁, s₂, hs₂, rfl⟩
    exact ins hs₁ (ih hs₂)
Induction Principle for Infimum of Filters
Informal description
Let $(f_i)_{i \in \iota}$ be a family of filters on a type $\alpha$, and let $s$ be a set in $\alpha$ such that $s$ belongs to the infimum filter $\bigsqcap_{i \in \iota} f_i$. Suppose $p$ is a predicate on sets in $\alpha$ satisfying: 1. $p$ holds for the universal set (i.e., $p(\text{univ})$), and 2. For any index $i \in \iota$ and sets $s_1, s_2 \subseteq \alpha$, if $s_1 \in f_i$ and $p(s_2)$ holds, then $p(s_1 \cap s_2)$ also holds. Then $p(s)$ holds.
Filter.iInf_principal_finset theorem
{ι : Type w} (s : Finset ι) (f : ι → Set α) : ⨅ i ∈ s, 𝓟 (f i) = 𝓟 (⋂ i ∈ s, f i)
Full source 
@[simp]
theorem iInf_principal_finset {ι : Type w} (s : Finset ι) (f : ι → Set α) :
    ⨅ i ∈ s, 𝓟 (f i) = 𝓟 (⋂ i ∈ s, f i) := by
  classical
  induction' s using Finset.induction_on with i s _ hs
  · simp
  · rw [Finset.iInf_insert, Finset.set_biInter_insert, hs, inf_principal]
Infimum of Principal Filters over a Finite Set Equals Principal Filter of Intersection
Informal description
For any finite set $s$ of type $\iota$ and any family of sets $f : \iota \to \text{Set} \alpha$, the infimum of the principal filters generated by $f(i)$ for $i \in s$ is equal to the principal filter generated by the intersection of all $f(i)$ for $i \in s$. In symbols: \[ \bigsqcap_{i \in s} \mathcal{P}(f(i)) = \mathcal{P}\left(\bigcap_{i \in s} f(i)\right) \]
Filter.iInf_principal theorem
{ι : Sort w} [Finite ι] (f : ι → Set α) : ⨅ i, 𝓟 (f i) = 𝓟 (⋂ i, f i)
Full source 
theorem iInf_principal {ι : Sort w} [Finite ι] (f : ι → Set α) : ⨅ i, 𝓟 (f i) = 𝓟 (⋂ i, f i) := by
  cases nonempty_fintype (PLift ι)
  rw [← iInf_plift_down, ← iInter_plift_down]
  simpa using iInf_principal_finset Finset.univ (f <| PLift.down ·)
Infimum of Principal Filters over Finite Type Equals Principal Filter of Intersection
Informal description
For any finite type $\iota$ and any family of sets $f : \iota \to \mathcal{P}(\alpha)$, the infimum of the principal filters generated by $f(i)$ for all $i \in \iota$ is equal to the principal filter generated by the intersection of all $f(i)$. In symbols: \[ \bigsqcap_{i \in \iota} \mathcal{P}(f(i)) = \mathcal{P}\left(\bigcap_{i \in \iota} f(i)\right) \]
Filter.iInf_principal' theorem
{ι : Type w} [Finite ι] (f : ι → Set α) : ⨅ i, 𝓟 (f i) = 𝓟 (⋂ i, f i)
Full source 
/-- A special case of `iInf_principal` that is safe to mark `simp`. -/
@[simp]
theorem iInf_principal' {ι : Type w} [Finite ι] (f : ι → Set α) : ⨅ i, 𝓟 (f i) = 𝓟 (⋂ i, f i) :=
  iInf_principal _
Infimum of Principal Filters over Finite Type Equals Principal Filter of Intersection
Informal description
For any finite type $\iota$ and any family of sets $f : \iota \to \mathcal{P}(\alpha)$, the infimum of the principal filters generated by $f(i)$ for all $i \in \iota$ is equal to the principal filter generated by the intersection of all $f(i)$. In symbols: \[ \bigsqcap_{i \in \iota} \mathcal{P}(f(i)) = \mathcal{P}\left(\bigcap_{i \in \iota} f(i)\right) \]
Filter.iInf_principal_finite theorem
{ι : Type w} {s : Set ι} (hs : s.Finite) (f : ι → Set α) : ⨅ i ∈ s, 𝓟 (f i) = 𝓟 (⋂ i ∈ s, f i)
Full source 
theorem iInf_principal_finite {ι : Type w} {s : Set ι} (hs : s.Finite) (f : ι → Set α) :
    ⨅ i ∈ s, 𝓟 (f i) = 𝓟 (⋂ i ∈ s, f i) := by
  lift s to Finset ι using hs
  exact mod_cast iInf_principal_finset s f
Infimum of Principal Filters over a Finite Set Equals Principal Filter of Intersection
Informal description
For any finite set $s$ of type $\iota$ and any family of sets $f : \iota \to \text{Set} \alpha$, the infimum of the principal filters generated by $f(i)$ for $i \in s$ is equal to the principal filter generated by the intersection of all $f(i)$ for $i \in s$. In symbols: \[ \bigsqcap_{i \in s} \mathcal{P}(f(i)) = \mathcal{P}\left(\bigcap_{i \in s} f(i)\right) \]
Filter.eventually_all theorem
{ι : Sort*} [Finite ι] {l} {p : ι → α → Prop} : (∀ᶠ x in l, ∀ i, p i x) ↔ ∀ i, ∀ᶠ x in l, p i x
Full source 
@[simp]
theorem eventually_all {ι : Sort*} [Finite ι] {l} {p : ι → α → Prop} :
    (∀ᶠ x in l, ∀ i, p i x) ↔ ∀ i, ∀ᶠ x in l, p i x := by
  simpa only [Filter.Eventually, setOf_forall] using iInter_mem
Finite Universal Quantifier Commutation with Filter Eventuality
Informal description
Let $\iota$ be a finite type, $l$ be a filter on a type $\alpha$, and $p : \iota \to \alpha \to \text{Prop}$ be a family of predicates. Then the following are equivalent: 1. For eventually all $x$ in $l$, for every $i \in \iota$, the predicate $p(i, x)$ holds. 2. For every $i \in \iota$, for eventually all $x$ in $l$, the predicate $p(i, x)$ holds. In symbols: $$\left(\forall^l x, \forall i, p(i, x)\right) \leftrightarrow \left(\forall i, \forall^l x, p(i, x)\right)$$
Filter.eventually_all_finite theorem
{ι} {I : Set ι} (hI : I.Finite) {l} {p : ι → α → Prop} : (∀ᶠ x in l, ∀ i ∈ I, p i x) ↔ ∀ i ∈ I, ∀ᶠ x in l, p i x
Full source 
@[simp]
theorem eventually_all_finite {ι} {I : Set ι} (hI : I.Finite) {l} {p : ι → α → Prop} :
    (∀ᶠ x in l, ∀ i ∈ I, p i x) ↔ ∀ i ∈ I, ∀ᶠ x in l, p i x := by
  simpa only [Filter.Eventually, setOf_forall] using biInter_mem hI
Finite Universal Quantifier Commutation with Filter Eventuality
Informal description
Let $I$ be a finite set of indices, $l$ be a filter on a type $\alpha$, and $p : \iota \to \alpha \to \text{Prop}$ be a family of predicates. Then the following are equivalent: 1. For eventually all $x$ in $l$, for every $i \in I$, the predicate $p(i, x)$ holds. 2. For every $i \in I$, for eventually all $x$ in $l$, the predicate $p(i, x)$ holds. In symbols: $$\left(\forall^l x, \forall i \in I, p(i, x)\right) \leftrightarrow \left(\forall i \in I, \forall^l x, p(i, x)\right)$$
Filter.eventually_all_finset theorem
{ι} (I : Finset ι) {l} {p : ι → α → Prop} : (∀ᶠ x in l, ∀ i ∈ I, p i x) ↔ ∀ i ∈ I, ∀ᶠ x in l, p i x
Full source 
@[simp] theorem eventually_all_finset {ι} (I : Finset ι) {l} {p : ι → α → Prop} :
    (∀ᶠ x in l, ∀ i ∈ I, p i x) ↔ ∀ i ∈ I, ∀ᶠ x in l, p i x :=
  I.finite_toSet.eventually_all
Finset Universal Quantifier Commutation with Filter Eventuality
Informal description
Let $I$ be a finite set of indices (represented as a finset), $l$ be a filter on a type $\alpha$, and $p : \iota \to \alpha \to \text{Prop}$ be a family of predicates. Then the following are equivalent: 1. For eventually all $x$ in $l$, for every $i \in I$, the predicate $p(i, x)$ holds. 2. For every $i \in I$, for eventually all $x$ in $l$, the predicate $p(i, x)$ holds. In symbols: $$\left(\forall^l x, \forall i \in I, p(i, x)\right) \leftrightarrow \left(\forall i \in I, \forall^l x, p(i, x)\right)$$
Filter.EventuallyLE.iUnion theorem
[Finite ι] {s t : ι → Set α} (h : ∀ i, s i ≤ᶠ[l] t i) : (⋃ i, s i) ≤ᶠ[l] ⋃ i, t i
Full source 
protected lemma EventuallyLE.iUnion [Finite ι] {s t : ι → Set α}
    (h : ∀ i, s i ≤ᶠ[l] t i) : (⋃ i, s i) ≤ᶠ[l] ⋃ i, t i :=
  (eventually_all.2 h).mono fun _x hx hx' ↦
    let ⟨i, hi⟩ := mem_iUnion.1 hx'; mem_iUnion.2 ⟨i, hx i hi⟩
Finite Union Preserves Eventual Containment under Filter
Informal description
Let $\iota$ be a finite type, $l$ be a filter on a type $\alpha$, and $s, t : \iota \to \text{Set } \alpha$ be families of sets. If for every $i \in \iota$, the set $s(i)$ is eventually contained in $t(i)$ with respect to the filter $l$, then the union $\bigcup_{i} s(i)$ is eventually contained in the union $\bigcup_{i} t(i)$ with respect to $l$. In symbols: $$\left(\forall i, s(i) \leq^l t(i)\right) \implies \left(\bigcup_i s(i) \leq^l \bigcup_i t(i)\right)$$
Filter.EventuallyEq.iUnion theorem
[Finite ι] {s t : ι → Set α} (h : ∀ i, s i =ᶠ[l] t i) : (⋃ i, s i) =ᶠ[l] ⋃ i, t i
Full source 
protected lemma EventuallyEq.iUnion [Finite ι] {s t : ι → Set α}
    (h : ∀ i, s i =ᶠ[l] t i) : (⋃ i, s i) =ᶠ[l] ⋃ i, t i :=
  (EventuallyLE.iUnion fun i ↦ (h i).le).antisymm <| .iUnion fun i ↦ (h i).symm.le
Finite Union Preserves Eventual Equality under Filter
Informal description
Let $\iota$ be a finite type, $l$ be a filter on a type $\alpha$, and $s, t : \iota \to \text{Set } \alpha$ be families of sets. If for every $i \in \iota$, the sets $s(i)$ and $t(i)$ are eventually equal with respect to the filter $l$, then their unions $\bigcup_{i} s(i)$ and $\bigcup_{i} t(i)$ are also eventually equal with respect to $l$. In symbols: $$\left(\forall i, s(i) =^l t(i)\right) \implies \left(\bigcup_i s(i) =^l \bigcup_i t(i)\right)$$
Filter.EventuallyLE.iInter theorem
[Finite ι] {s t : ι → Set α} (h : ∀ i, s i ≤ᶠ[l] t i) : (⋂ i, s i) ≤ᶠ[l] ⋂ i, t i
Full source 
protected lemma EventuallyLE.iInter [Finite ι] {s t : ι → Set α}
    (h : ∀ i, s i ≤ᶠ[l] t i) : (⋂ i, s i) ≤ᶠ[l] ⋂ i, t i :=
  (eventually_all.2 h).mono fun _x hx hx' ↦ mem_iInter.2 fun i ↦ hx i (mem_iInter.1 hx' i)
Finite Intersection Preserves Eventual Containment under Filter
Informal description
Let $\iota$ be a finite type, $l$ be a filter on a type $\alpha$, and $s, t : \iota \to \text{Set } \alpha$ be families of sets. If for every $i \in \iota$, the set $s(i)$ is eventually contained in $t(i)$ with respect to the filter $l$, then the intersection $\bigcap_{i} s(i)$ is eventually contained in the intersection $\bigcap_{i} t(i)$ with respect to $l$. In symbols: $$\left(\forall i, s(i) \leq^l t(i)\right) \implies \left(\bigcap_i s(i) \leq^l \bigcap_i t(i)\right)$$
Filter.EventuallyEq.iInter theorem
[Finite ι] {s t : ι → Set α} (h : ∀ i, s i =ᶠ[l] t i) : (⋂ i, s i) =ᶠ[l] ⋂ i, t i
Full source 
protected lemma EventuallyEq.iInter [Finite ι] {s t : ι → Set α}
    (h : ∀ i, s i =ᶠ[l] t i) : (⋂ i, s i) =ᶠ[l] ⋂ i, t i :=
  (EventuallyLE.iInter fun i ↦ (h i).le).antisymm <| .iInter fun i ↦ (h i).symm.le
Finite Intersection Preserves Eventual Equality under Filter
Informal description
Let $\iota$ be a finite type, $l$ be a filter on a type $\alpha$, and $s, t : \iota \to \text{Set } \alpha$ be families of sets. If for every $i \in \iota$, the sets $s(i)$ and $t(i)$ are eventually equal with respect to the filter $l$, then the intersections $\bigcap_{i} s(i)$ and $\bigcap_{i} t(i)$ are also eventually equal with respect to $l$. In symbols: $$\left(\forall i, s(i) =^l t(i)\right) \implies \left(\bigcap_i s(i) =^l \bigcap_i t(i)\right)$$
Set.Finite.eventuallyLE_iUnion theorem
{ι : Type*} {s : Set ι} (hs : s.Finite) {f g : ι → Set α} (hle : ∀ i ∈ s, f i ≤ᶠ[l] g i) : (⋃ i ∈ s, f i) ≤ᶠ[l] (⋃ i ∈ s, g i)
Full source 
lemma _root_.Set.Finite.eventuallyLE_iUnion {ι : Type*} {s : Set ι} (hs : s.Finite)
    {f g : ι → Set α} (hle : ∀ i ∈ s, f i ≤ᶠ[l] g i) : (⋃ i ∈ s, f i) ≤ᶠ[l] (⋃ i ∈ s, g i) := by
  have := hs.to_subtype
  rw [biUnion_eq_iUnion, biUnion_eq_iUnion]
  exact .iUnion fun i ↦ hle i.1 i.2
Finite Union Preserves Eventual Containment under Filter for Subset
Informal description
Let $\iota$ be a type, $s \subseteq \iota$ be a finite subset, and $l$ be a filter on a type $\alpha$. For any families of sets $f, g : \iota \to \text{Set } \alpha$, if for every $i \in s$ the set $f(i)$ is eventually contained in $g(i)$ with respect to $l$, then the union $\bigcup_{i \in s} f(i)$ is eventually contained in the union $\bigcup_{i \in s} g(i)$ with respect to $l$. In symbols: $$(\forall i \in s, f(i) \leq^l g(i)) \implies \left(\bigcup_{i \in s} f(i) \leq^l \bigcup_{i \in s} g(i)\right)$$
Set.Finite.eventuallyEq_iUnion theorem
{ι : Type*} {s : Set ι} (hs : s.Finite) {f g : ι → Set α} (heq : ∀ i ∈ s, f i =ᶠ[l] g i) : (⋃ i ∈ s, f i) =ᶠ[l] (⋃ i ∈ s, g i)
Full source 
lemma _root_.Set.Finite.eventuallyEq_iUnion {ι : Type*} {s : Set ι} (hs : s.Finite)
    {f g : ι → Set α} (heq : ∀ i ∈ s, f i =ᶠ[l] g i) : (⋃ i ∈ s, f i) =ᶠ[l] (⋃ i ∈ s, g i) :=
  (EventuallyLE.biUnion hs fun i hi ↦ (heq i hi).le).antisymm <|
    .biUnion hs fun i hi ↦ (heq i hi).symm.le
Finite Union Preserves Eventual Equality under Filter for Subset of Indices
Informal description
Let $\iota$ be a type, $s \subseteq \iota$ be a finite subset, and $l$ be a filter on a type $\alpha$. For any families of sets $f, g : \iota \to \text{Set } \alpha$, if for every $i \in s$ the sets $f(i)$ and $g(i)$ are eventually equal with respect to $l$, then the unions $\bigcup_{i \in s} f(i)$ and $\bigcup_{i \in s} g(i)$ are also eventually equal with respect to $l$. In symbols: $$(\forall i \in s, f(i) =^l g(i)) \implies \left(\bigcup_{i \in s} f(i) =^l \bigcup_{i \in s} g(i)\right)$$
Set.Finite.eventuallyLE_iInter theorem
{ι : Type*} {s : Set ι} (hs : s.Finite) {f g : ι → Set α} (hle : ∀ i ∈ s, f i ≤ᶠ[l] g i) : (⋂ i ∈ s, f i) ≤ᶠ[l] (⋂ i ∈ s, g i)
Full source 
lemma _root_.Set.Finite.eventuallyLE_iInter {ι : Type*} {s : Set ι} (hs : s.Finite)
    {f g : ι → Set α} (hle : ∀ i ∈ s, f i ≤ᶠ[l] g i) : (⋂ i ∈ s, f i) ≤ᶠ[l] (⋂ i ∈ s, g i) := by
  have := hs.to_subtype
  rw [biInter_eq_iInter, biInter_eq_iInter]
  exact .iInter fun i ↦ hle i.1 i.2
Finite Intersection Preserves Eventual Containment under Filter for Subset of Indices
Informal description
Let $\iota$ be a type, $s \subseteq \iota$ be a finite subset, $l$ be a filter on a type $\alpha$, and $f, g : \iota \to \text{Set } \alpha$ be families of sets. If for every $i \in s$, the set $f(i)$ is eventually contained in $g(i)$ with respect to the filter $l$, then the intersection $\bigcap_{i \in s} f(i)$ is eventually contained in the intersection $\bigcap_{i \in s} g(i)$ with respect to $l$. In symbols: $$(\forall i \in s, f(i) \leq^l g(i)) \implies \left(\bigcap_{i \in s} f(i) \leq^l \bigcap_{i \in s} g(i)\right)$$
Set.Finite.eventuallyEq_iInter theorem
{ι : Type*} {s : Set ι} (hs : s.Finite) {f g : ι → Set α} (heq : ∀ i ∈ s, f i =ᶠ[l] g i) : (⋂ i ∈ s, f i) =ᶠ[l] (⋂ i ∈ s, g i)
Full source 
lemma _root_.Set.Finite.eventuallyEq_iInter {ι : Type*} {s : Set ι} (hs : s.Finite)
    {f g : ι → Set α} (heq : ∀ i ∈ s, f i =ᶠ[l] g i) : (⋂ i ∈ s, f i) =ᶠ[l] (⋂ i ∈ s, g i) :=
  (EventuallyLE.biInter hs fun i hi ↦ (heq i hi).le).antisymm <|
    .biInter hs fun i hi ↦ (heq i hi).symm.le
Finite Intersection Preserves Eventual Equality under Filter for Subset of Indices
Informal description
Let $\iota$ be a type, $s \subseteq \iota$ be a finite subset, $l$ be a filter on a type $\alpha$, and $f, g : \iota \to \text{Set } \alpha$ be families of sets. If for every $i \in s$, the sets $f(i)$ and $g(i)$ are eventually equal with respect to the filter $l$, then the intersections $\bigcap_{i \in s} f(i)$ and $\bigcap_{i \in s} g(i)$ are also eventually equal with respect to $l$. In symbols: $$(\forall i \in s, f(i) =^l g(i)) \implies \left(\bigcap_{i \in s} f(i) =^l \bigcap_{i \in s} g(i)\right)$$
Finset.eventuallyLE_iUnion theorem
{ι : Type*} (s : Finset ι) {f g : ι → Set α} (hle : ∀ i ∈ s, f i ≤ᶠ[l] g i) : (⋃ i ∈ s, f i) ≤ᶠ[l] (⋃ i ∈ s, g i)
Full source 
lemma _root_.Finset.eventuallyLE_iUnion {ι : Type*} (s : Finset ι) {f g : ι → Set α}
    (hle : ∀ i ∈ s, f i ≤ᶠ[l] g i) : (⋃ i ∈ s, f i) ≤ᶠ[l] (⋃ i ∈ s, g i) :=
  .biUnion s.finite_toSet hle
Finite Union Preserves Eventual Containment under Filter
Informal description
Let $\iota$ be a type, $s$ be a finite set of indices of type $\iota$, and $l$ be a filter on a type $\alpha$. Given two families of sets $f, g : \iota \to \mathcal{P}(\alpha)$, if for every $i \in s$ the set $f(i)$ is eventually contained in $g(i)$ with respect to the filter $l$, then the union $\bigcup_{i \in s} f(i)$ is eventually contained in the union $\bigcup_{i \in s} g(i)$ with respect to $l$. In symbols: $$(\forall i \in s, f(i) \leq^l g(i)) \implies \left(\bigcup_{i \in s} f(i) \leq^l \bigcup_{i \in s} g(i)\right)$$
Finset.eventuallyEq_iUnion theorem
{ι : Type*} (s : Finset ι) {f g : ι → Set α} (heq : ∀ i ∈ s, f i =ᶠ[l] g i) : (⋃ i ∈ s, f i) =ᶠ[l] (⋃ i ∈ s, g i)
Full source 
lemma _root_.Finset.eventuallyEq_iUnion {ι : Type*} (s : Finset ι) {f g : ι → Set α}
    (heq : ∀ i ∈ s, f i =ᶠ[l] g i) : (⋃ i ∈ s, f i) =ᶠ[l] (⋃ i ∈ s, g i) :=
  .biUnion s.finite_toSet heq
Finite Union Preserves Eventual Equality under Filter
Informal description
Let $\iota$ be a type, $s$ be a finite set of indices of type $\iota$, and $l$ be a filter on a type $\alpha$. Given two families of sets $f, g : \iota \to \mathcal{P}(\alpha)$, if for every $i \in s$ the sets $f(i)$ and $g(i)$ are eventually equal with respect to the filter $l$, then the unions $\bigcup_{i \in s} f(i)$ and $\bigcup_{i \in s} g(i)$ are also eventually equal with respect to $l$. In symbols: $$(\forall i \in s, f(i) =^l g(i)) \implies \left(\bigcup_{i \in s} f(i) =^l \bigcup_{i \in s} g(i)\right)$$
Finset.eventuallyLE_iInter theorem
{ι : Type*} (s : Finset ι) {f g : ι → Set α} (hle : ∀ i ∈ s, f i ≤ᶠ[l] g i) : (⋂ i ∈ s, f i) ≤ᶠ[l] (⋂ i ∈ s, g i)
Full source 
lemma _root_.Finset.eventuallyLE_iInter {ι : Type*} (s : Finset ι) {f g : ι → Set α}
    (hle : ∀ i ∈ s, f i ≤ᶠ[l] g i) : (⋂ i ∈ s, f i) ≤ᶠ[l] (⋂ i ∈ s, g i) :=
  .biInter s.finite_toSet hle
Finite Intersection Preserves Eventual Inequality
Informal description
For any finite set $s$ of indices of type $\iota$ and any family of sets $f, g \colon \iota \to \mathcal{P}(\alpha)$, if for every $i \in s$ the set $f(i)$ is eventually less than or equal to $g(i)$ with respect to a filter $l$, then the intersection $\bigcap_{i \in s} f(i)$ is eventually less than or equal to the intersection $\bigcap_{i \in s} g(i)$ with respect to the same filter $l$.
Finset.eventuallyEq_iInter theorem
{ι : Type*} (s : Finset ι) {f g : ι → Set α} (heq : ∀ i ∈ s, f i =ᶠ[l] g i) : (⋂ i ∈ s, f i) =ᶠ[l] (⋂ i ∈ s, g i)
Full source 
lemma _root_.Finset.eventuallyEq_iInter {ι : Type*} (s : Finset ι) {f g : ι → Set α}
    (heq : ∀ i ∈ s, f i =ᶠ[l] g i) : (⋂ i ∈ s, f i) =ᶠ[l] (⋂ i ∈ s, g i) :=
  .biInter s.finite_toSet heq
Finite Intersection Preserves Eventual Equality
Informal description
For any finite set $s$ of indices of type $\iota$ and any family of sets $f, g \colon \iota \to \mathcal{P}(\alpha)$, if for every $i \in s$ the set $f(i)$ is eventually equal to $g(i)$ with respect to a filter $l$, then the intersection $\bigcap_{i \in s} f(i)$ is eventually equal to the intersection $\bigcap_{i \in s} g(i)$ with respect to the same filter $l$.