Documentation

Mathlib.Order.Filter.Finite

Results relating filters to finiteness #

This file proves that finitely many conditions eventually hold if each of them eventually holds.

source
@[simp]
theorem Filter.biInter_mem {α : Type u} {f : Filter α} {β : Type v} {s : β → Set α} {is : Set β} (hf : is.Finite) :
⋂ i ∈ is, s i ∈ f ↔ ∀ i ∈ is, s i ∈ f
source
@[simp]
theorem Filter.biInter_finset_mem {α : Type u} {f : Filter α} {β : Type v} {s : β → Set α} (is : Finset β) :
⋂ i ∈ is, s i ∈ f ↔ ∀ i ∈ is, s i ∈ f
source
theorem Finset.iInter_mem_sets {α : Type u} {f : Filter α} {β : Type v} {s : β → Set α} (is : Finset β) :
⋂ i ∈ is, s i ∈ f ↔ ∀ i ∈ is, s i ∈ f

Alias of Filter.biInter_finset_mem.

source
@[simp]
theorem Filter.sInter_mem {α : Type u} {f : Filter α} {s : Set (Set α)} (hfin : s.Finite) :
⋂₀ s ∈ f ↔ ∀ U ∈ s, U ∈ f
source
@[simp]
theorem Filter.iInter_mem {α : Type u} {f : Filter α} {β : Sort v} {s : β → Set α} [Finite β] :
⋂ (i : β), s i ∈ f ↔ ∀ (i : β), s i ∈ f
source
theorem Filter.mem_generate_iff {α : Type u} {s : Set (Set α)} {U : Set α} :
U ∈ generate s ↔ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U
source
theorem Filter.mem_iInf_of_iInter {α : Type u} {ι : Type u_1} {s : ι → Filter α} {U : Set α} {I : Set ι} (I_fin : I.Finite) {V : ↑I → Set α} (hV : ∀ (i : ↑I), V i ∈ s ↑i) (hU : ⋂ (i : ↑I), V i ⊆ U) :
U ∈ ⨅ (i : ι), s i
source
theorem Filter.mem_iInf {α : Type u} {ι : Type u_1} {s : ι → Filter α} {U : Set α} :
U ∈ ⨅ (i : ι), s i ↔ ∃ (I : Set ι), I.Finite ∧ ∃ (V : ↑I → Set α), (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ (i : ↑I), V i
source
theorem Filter.mem_iInf' {α : Type u} {ι : Type u_1} {s : ι → Filter α} {U : Set α} :
U ∈ ⨅ (i : ι), s i ↔ ∃ (I : Set ι), I.Finite ∧ ∃ (V : ι → Set α), (∀ (i : ι), V i ∈ s i) ∧ (∀ i ∉ I, V i = Set.univ) ∧ U = ⋂ i ∈ I, V i ∧ U = ⋂ (i : ι), V i
source
theorem Filter.exists_iInter_of_mem_iInf {ι : Sort u_1} {α : Type u_2} {f : ι → Filter α} {s : Set α} (hs : s ∈ ⨅ (i : ι), f i) :
∃ (t : ι → Set α), (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ (i : ι), t i
source
theorem Filter.mem_iInf_of_finite {ι : Sort u_1} [Finite ι] {α : Type u_2} {f : ι → Filter α} (s : Set α) :
s ∈ ⨅ (i : ι), f i ↔ ∃ (t : ι → Set α), (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ (i : ι), t i
source
theorem Filter.mem_biInf_principal {α : Type u} {ι : Type u_1} {p : ι → Prop} {s : ι → Set α} {t : Set α} :
t ∈ ⨅ (i : ι), ⨅ (_ : p i), principal (s i) ↔ ∃ (I : Set ι), I.Finite ∧ (∀ i ∈ I, p i) ∧ ⋂ i ∈ I, s i ⊆ t

Lattice equations #

source
theorem Pairwise.exists_mem_filter_of_disjoint {α : Type u} {ι : Type u_1} [Finite ι] {l : ι → Filter α} (hd : Pairwise (Function.onFun Disjoint l)) :
∃ (s : ι → Set α), (∀ (i : ι), s i ∈ l i) ∧ Pairwise (Function.onFun Disjoint s)
source
theorem Set.PairwiseDisjoint.exists_mem_filter {α : Type u} {ι : Type u_1} {l : ι → Filter α} {t : Set ι} (hd : t.PairwiseDisjoint l) (ht : t.Finite) :
∃ (s : ι → Set α), (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s
source
theorem Filter.iInf_sets_eq_finite {α : Type u} {ι : Type u_1} (f : ι → Filter α) :
(⨅ (i : ι), f i).sets = ⋃ (t : Finset ι), (⨅ i ∈ t, f i).sets
source
theorem Filter.iInf_sets_eq_finite' {α : Type u} {ι : Sort x} (f : ι → Filter α) :
(⨅ (i : ι), f i).sets = ⋃ (t : Finset (PLift ι)), (⨅ i ∈ t, f i.down).sets
source
theorem Filter.mem_iInf_finite {α : Type u} {ι : Type u_1} {f : ι → Filter α} (s : Set α) :
s ∈ iInf f ↔ ∃ (t : Finset ι), s ∈ ⨅ i ∈ t, f i
source
theorem Filter.mem_iInf_finite' {α : Type u} {ι : Sort x} {f : ι → Filter α} (s : Set α) :
s ∈ iInf f ↔ ∃ (t : Finset (PLift ι)), s ∈ ⨅ i ∈ t, f i.down
source
theorem Filter.mem_iInf_finset {α : Type u} {β : Type v} {s : Finset α} {f : α → Filter β} {t : Set β} :
t ∈ ⨅ a ∈ s, f a ↔ ∃ (p : α → Set β), (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ a ∈ s, p a

principal equations #

source
@[simp]
theorem Filter.iInf_principal_finset {α : Type u} {ι : Type w} (s : Finset ι) (f : ι → Set α) :
⨅ i ∈ s, principal (f i) = principal (⋂ i ∈ s, f i)
source
theorem Filter.iInf_principal {α : Type u} {ι : Sort w} [Finite ι] (f : ι → Set α) :
⨅ (i : ι), principal (f i) = principal (⋂ (i : ι), f i)
source
@[simp]
theorem Filter.iInf_principal' {α : Type u} {ι : Type w} [Finite ι] (f : ι → Set α) :
⨅ (i : ι), principal (f i) = principal (⋂ (i : ι), f i)

A special case of iInf_principal that is safe to mark simp.

source
theorem Filter.iInf_principal_finite {α : Type u} {ι : Type w} {s : Set ι} (hs : s.Finite) (f : ι → Set α) :
⨅ i ∈ s, principal (f i) = principal (⋂ i ∈ s, f i)
source
theorem Filter.eq_principal_of_finite_sets {α : Type u} {f : Filter α} (hf : f.sets.Finite) :
∃ (s : Set α), f = principal s

If a filter has finitely many sets, then it is principal.

source
theorem Filter.eq_principal_of_finite {α : Type u} [Finite α] (f : Filter α) :
∃ (s : Set α), f = principal s

Any filter on a finite type is principal.

source
theorem Filter.principal_surjective {α : Type u} [Finite α] :
Function.Surjective principal

Eventually and Frequently #

source
@[simp]
theorem Filter.eventually_all {α : Type u} {ι : Sort u_1} [Finite ι] {l : Filter α} {p : ι → α → Prop} :
(∀ᶠ (x : α) in l, ∀ (i : ι), p i x) ↔ ∀ (i : ι), ∀ᶠ (x : α) in l, p i x
source
@[simp]
theorem Filter.eventually_all_finite {α : Type u} {ι : Type u_1} {I : Set ι} (hI : I.Finite) {l : Filter α} {p : ι → α → Prop} :
(∀ᶠ (x : α) in l, ∀ i ∈ I, p i x) ↔ ∀ i ∈ I, ∀ᶠ (x : α) in l, p i x
source
theorem Set.Finite.eventually_all {α : Type u} {ι : Type u_1} {I : Set ι} (hI : I.Finite) {l : Filter α} {p : ι → α → Prop} :
(∀ᶠ (x : α) in l, ∀ i ∈ I, p i x) ↔ ∀ i ∈ I, ∀ᶠ (x : α) in l, p i x

Alias of Filter.eventually_all_finite.

source
@[simp]
theorem Filter.eventually_all_finset {α : Type u} {ι : Type u_1} (I : Finset ι) {l : Filter α} {p : ι → α → Prop} :
(∀ᶠ (x : α) in l, ∀ i ∈ I, p i x) ↔ ∀ i ∈ I, ∀ᶠ (x : α) in l, p i x
source
theorem Finset.eventually_all {α : Type u} {ι : Type u_1} (I : Finset ι) {l : Filter α} {p : ι → α → Prop} :
(∀ᶠ (x : α) in l, ∀ i ∈ I, p i x) ↔ ∀ i ∈ I, ∀ᶠ (x : α) in l, p i x

Alias of Filter.eventually_all_finset.

source
@[simp]
theorem Filter.frequently_exists {α : Type u} {ι : Sort u_1} [Finite ι] {l : Filter α} {p : ι → α → Prop} :
(∃ᶠ (x : α) in l, ∃ (i : ι), p i x) ↔ ∃ (i : ι), ∃ᶠ (x : α) in l, p i x
source
@[simp]
theorem Filter.frequently_exists_finite {α : Type u} {ι : Type u_1} {I : Set ι} (hI : I.Finite) {l : Filter α} {p : ι → α → Prop} :
(∃ᶠ (x : α) in l, ∃ i ∈ I, p i x) ↔ ∃ i ∈ I, ∃ᶠ (x : α) in l, p i x
source
theorem Set.Finite.frequently_exists {α : Type u} {ι : Type u_1} {I : Set ι} (hI : I.Finite) {l : Filter α} {p : ι → α → Prop} :
(∃ᶠ (x : α) in l, ∃ i ∈ I, p i x) ↔ ∃ i ∈ I, ∃ᶠ (x : α) in l, p i x

Alias of Filter.frequently_exists_finite.

source
@[simp]
theorem Filter.frequently_exists_finset {α : Type u} {ι : Type u_1} (I : Finset ι) {l : Filter α} {p : ι → α → Prop} :
(∃ᶠ (x : α) in l, ∃ i ∈ I, p i x) ↔ ∃ i ∈ I, ∃ᶠ (x : α) in l, p i x
source
theorem Finset.frequently_exists {α : Type u} {ι : Type u_1} (I : Finset ι) {l : Filter α} {p : ι → α → Prop} :
(∃ᶠ (x : α) in l, ∃ i ∈ I, p i x) ↔ ∃ i ∈ I, ∃ᶠ (x : α) in l, p i x

Alias of Filter.frequently_exists_finset.

source
theorem Filter.eventually_subset_of_finite {α : Type u} {ι : Type u_1} {f : Filter ι} {s : ι → Set α} {t : Set α} (ht : t.Finite) (hs : ∀ a ∈ t, ∀ᶠ (i : ι) in f, a ∈ s i) :
∀ᶠ (i : ι) in f, t ⊆ s i

Relation “eventually equal” #

source
theorem Filter.EventuallySubset.iUnion {α : Type u} {ι : Sort x} {l : Filter α} [Finite ι] {s t : ι → Set α} (h : ∀ (i : ι), s i ≤ᶠ[l] t i) :
⋃ (i : ι), s i ≤ᶠ[l] ⋃ (i : ι), t i
source
theorem Filter.EventuallyEqSet.iUnion {α : Type u} {ι : Sort x} {l : Filter α} [Finite ι] {s t : ι → Set α} (h : ∀ (i : ι), s i =ᶠ[l] t i) :
⋃ (i : ι), s i =ᶠ[l] ⋃ (i : ι), t i
source
theorem Filter.EventuallySubset.iInter {α : Type u} {ι : Sort x} {l : Filter α} [Finite ι] {s t : ι → Set α} (h : ∀ (i : ι), s i ≤ᶠ[l] t i) :
⋂ (i : ι), s i ≤ᶠ[l] ⋂ (i : ι), t i
source
theorem Filter.EventuallyEqSet.iInter {α : Type u} {ι : Sort x} {l : Filter α} [Finite ι] {s t : ι → Set α} (h : ∀ (i : ι), s i =ᶠ[l] t i) :
⋂ (i : ι), s i =ᶠ[l] ⋂ (i : ι), t i
source
theorem Set.Finite.eventuallySubset_iUnion {α : Type u} {l : Filter α} {ι : Type u_1} {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
source
theorem Filter.EventuallySubset.biUnion {α : Type u} {l : Filter α} {ι : Type u_1} {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

Alias of Set.Finite.eventuallySubset_iUnion.

source
@[deprecated Set.Finite.eventuallySubset_iUnion (since := "2026-08-14")]
theorem Set.Finite.eventuallyLE_iUnion {α : Type u} {l : Filter α} {ι : Type u_1} {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

Alias of Set.Finite.eventuallySubset_iUnion.

source
theorem Set.Finite.eventuallyEqSet_iUnion {α : Type u} {l : Filter α} {ι : Type u_1} {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
source
theorem Filter.EventuallyEqSet.biUnion {α : Type u} {l : Filter α} {ι : Type u_1} {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

Alias of Set.Finite.eventuallyEqSet_iUnion.

source
@[deprecated Set.Finite.eventuallyEqSet_iUnion (since := "2026-08-14")]
theorem Set.Finite.eventuallyEq_iUnion {α : Type u} {l : Filter α} {ι : Type u_1} {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

Alias of Set.Finite.eventuallyEqSet_iUnion.

source
theorem Set.Finite.eventuallySubset_iInter {α : Type u} {l : Filter α} {ι : Type u_1} {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
source
theorem Filter.EventuallySubset.biInter {α : Type u} {l : Filter α} {ι : Type u_1} {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

Alias of Set.Finite.eventuallySubset_iInter.

source
@[deprecated Set.Finite.eventuallySubset_iInter (since := "2026-08-14")]
theorem Set.Finite.eventuallyLE_iInter {α : Type u} {l : Filter α} {ι : Type u_1} {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

Alias of Set.Finite.eventuallySubset_iInter.

source
theorem Set.Finite.eventuallyEqSet_iInter {α : Type u} {l : Filter α} {ι : Type u_1} {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
source
theorem Filter.EventuallyEqSet.biInter {α : Type u} {l : Filter α} {ι : Type u_1} {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

Alias of Set.Finite.eventuallyEqSet_iInter.

source
@[deprecated Set.Finite.eventuallyEqSet_iInter (since := "2026-08-14")]
theorem Set.Finite.eventuallyEq_iInter {α : Type u} {l : Filter α} {ι : Type u_1} {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

Alias of Set.Finite.eventuallyEqSet_iInter.

source
theorem Finset.eventuallySubset_iUnion {α : Type u} {l : Filter α} {ι : Type u_1} (s : Finset ι) {f g : ι → Set α} (hle : ∀ i ∈ s, f i ≤ᶠ[l] g i) :
⋃ i ∈ s, f i ≤ᶠ[l] ⋃ i ∈ s, g i
source
@[deprecated Finset.eventuallySubset_iUnion (since := "2026-08-14")]
theorem Finset.eventuallyLE_iUnion {α : Type u} {l : Filter α} {ι : Type u_1} (s : Finset ι) {f g : ι → Set α} (hle : ∀ i ∈ s, f i ≤ᶠ[l] g i) :
⋃ i ∈ s, f i ≤ᶠ[l] ⋃ i ∈ s, g i

Alias of Finset.eventuallySubset_iUnion.

source
theorem Finset.eventuallyEqSet_iUnion {α : Type u} {l : Filter α} {ι : Type u_1} (s : Finset ι) {f g : ι → Set α} (heq : ∀ i ∈ s, f i =ᶠ[l] g i) :
⋃ i ∈ s, f i =ᶠ[l] ⋃ i ∈ s, g i
source
@[deprecated Finset.eventuallyEqSet_iUnion (since := "2026-08-14")]
theorem Finset.eventuallyEq_iUnion {α : Type u} {l : Filter α} {ι : Type u_1} (s : Finset ι) {f g : ι → Set α} (heq : ∀ i ∈ s, f i =ᶠ[l] g i) :
⋃ i ∈ s, f i =ᶠ[l] ⋃ i ∈ s, g i

Alias of Finset.eventuallyEqSet_iUnion.

source
theorem Finset.eventuallySubset_iInter {α : Type u} {l : Filter α} {ι : Type u_1} (s : Finset ι) {f g : ι → Set α} (hle : ∀ i ∈ s, f i ≤ᶠ[l] g i) :
⋂ i ∈ s, f i ≤ᶠ[l] ⋂ i ∈ s, g i
source
@[deprecated Finset.eventuallySubset_iInter (since := "2026-08-14")]
theorem Finset.eventuallyLE_iInter {α : Type u} {l : Filter α} {ι : Type u_1} (s : Finset ι) {f g : ι → Set α} (hle : ∀ i ∈ s, f i ≤ᶠ[l] g i) :
⋂ i ∈ s, f i ≤ᶠ[l] ⋂ i ∈ s, g i

Alias of Finset.eventuallySubset_iInter.

source
theorem Finset.eventuallyEqSet_iInter {α : Type u} {l : Filter α} {ι : Type u_1} (s : Finset ι) {f g : ι → Set α} (heq : ∀ i ∈ s, f i =ᶠ[l] g i) :
⋂ i ∈ s, f i =ᶠ[l] ⋂ i ∈ s, g i
source
@[deprecated Finset.eventuallyEqSet_iInter (since := "2026-08-14")]
theorem Finset.eventuallyEq_iInter {α : Type u} {l : Filter α} {ι : Type u_1} (s : Finset ι) {f g : ι → Set α} (heq : ∀ i ∈ s, f i =ᶠ[l] g i) :
⋂ i ∈ s, f i =ᶠ[l] ⋂ i ∈ s, g i

Alias of Finset.eventuallyEqSet_iInter.

source
@[deprecated Filter.EventuallySubset.iUnion (since := "2026-08-14")]
theorem Filter.EventuallyLE.iUnion {α : Type u} {ι : Sort x} {l : Filter α} [Finite ι] {s t : ι → Set α} (h : ∀ (i : ι), s i ≤ᶠ[l] t i) :
⋃ (i : ι), s i ≤ᶠ[l] ⋃ (i : ι), t i

Alias of Filter.EventuallySubset.iUnion.

source
@[deprecated Filter.EventuallyEqSet.iUnion (since := "2026-08-14")]
theorem Filter.EventuallyEq.iUnion {α : Type u} {ι : Sort x} {l : Filter α} [Finite ι] {s t : ι → Set α} (h : ∀ (i : ι), s i =ᶠ[l] t i) :
⋃ (i : ι), s i =ᶠ[l] ⋃ (i : ι), t i

Alias of Filter.EventuallyEqSet.iUnion.

source
@[deprecated Filter.EventuallySubset.iInter (since := "2026-08-14")]
theorem Filter.EventuallyLE.iInter {α : Type u} {ι : Sort x} {l : Filter α} [Finite ι] {s t : ι → Set α} (h : ∀ (i : ι), s i ≤ᶠ[l] t i) :
⋂ (i : ι), s i ≤ᶠ[l] ⋂ (i : ι), t i

Alias of Filter.EventuallySubset.iInter.

source
@[deprecated Filter.EventuallyEqSet.iInter (since := "2026-08-14")]
theorem Filter.EventuallyEq.iInter {α : Type u} {ι : Sort x} {l : Filter α} [Finite ι] {s t : ι → Set α} (h : ∀ (i : ι), s i =ᶠ[l] t i) :
⋂ (i : ι), s i =ᶠ[l] ⋂ (i : ι), t i

Alias of Filter.EventuallyEqSet.iInter.

source
@[deprecated Filter.EventuallySubset.biUnion (since := "2026-08-14")]
theorem Filter.EventuallyLE.biUnion {α : Type u} {l : Filter α} {ι : Type u_1} {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

Alias of Filter.EventuallySubset.biUnion.

Alias of Set.Finite.eventuallySubset_iUnion.

source
@[deprecated Filter.EventuallyEqSet.biUnion (since := "2026-08-14")]
theorem Filter.EventuallyEq.biUnion {α : Type u} {l : Filter α} {ι : Type u_1} {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

Alias of Filter.EventuallyEqSet.biUnion.

Alias of Set.Finite.eventuallyEqSet_iUnion.

source
@[deprecated Filter.EventuallySubset.biInter (since := "2026-08-14")]
theorem Filter.EventuallyLE.biInter {α : Type u} {l : Filter α} {ι : Type u_1} {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

Alias of Filter.EventuallySubset.biInter.

Alias of Set.Finite.eventuallySubset_iInter.

source
@[deprecated Filter.EventuallyEqSet.biInter (since := "2026-08-14")]
theorem Filter.EventuallyEq.biInter {α : Type u} {l : Filter α} {ι : Type u_1} {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

Alias of Filter.EventuallyEqSet.biInter.

Alias of Set.Finite.eventuallyEqSet_iInter.