Results relating filters to finiteness

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

@[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

@[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

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.

@[simp]

theorem Filter.sInter_mem {α : Type u} {f : Filter α} {s : Set (Set α)} (hfin : s.Finite) : ⋂₀ s ∈ f ↔ ∀ U ∈ s, U ∈ f

@[simp]

theorem Filter.iInter_mem {α : Type u} {f : Filter α} {β : Sort v} {s : β → Set α} [Finite β] : ⋂ (i : β), s i ∈ f ↔ ∀ (i : β), s i ∈ f

theorem Filter.mem_generate_iff {α : Type u} {s : Set (Set α)} {U : Set α} : U ∈ generate s ↔ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U

theorem Filter.mem_iInf_of_iInter {α : Type u} {ι : Type u_2} {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

theorem Filter.mem_iInf {α : Type u} {ι : Type u_2} {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

theorem Filter.mem_iInf' {α : Type u} {ι : Type u_2} {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

theorem Filter.exists_iInter_of_mem_iInf {ι : Sort u_2} {α : Type u_3} {f : ι → Filter α} {s : Set α} (hs : s ∈ ⨅ (i : ι), f i) : ∃ (t : ι → Set α), (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ (i : ι), t i

theorem Filter.mem_iInf_of_finite {ι : Sort u_2} [Finite ι] {α : Type u_3} {f : ι → Filter α} (s : Set α) : s ∈ ⨅ (i : ι), f i ↔ ∃ (t : ι → Set α), (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ (i : ι), t i

theorem Filter.mem_biInf_principal {α : Type u} {ι : Type u_2} {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

theorem Pairwise.exists_mem_filter_of_disjoint {α : Type u} {ι : Type u_2} [Finite ι] {l : ι → Filter α} (hd : Pairwise (Function.onFun Disjoint l)) : ∃ (s : ι → Set α), (∀ (i : ι), s i ∈ l i) ∧ Pairwise (Function.onFun Disjoint s)

theorem Set.PairwiseDisjoint.exists_mem_filter {α : Type u} {ι : Type u_2} {l : ι → Filter α} {t : Set ι} (hd : t.PairwiseDisjoint l) (ht : t.Finite) : ∃ (s : ι → Set α), (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s

theorem Filter.iInf_sets_eq_finite {α : Type u} {ι : Type u_2} (f : ι → Filter α) : (⨅ (i : ι), f i).sets = ⋃ (t : Finset ι), (⨅ i ∈ t, f i).sets

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

theorem Filter.mem_iInf_finite {α : Type u} {ι : Type u_2} {f : ι → Filter α} (s : Set α) : s ∈ iInf f ↔ ∃ (t : Finset ι), s ∈ ⨅ i ∈ t, f i

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

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

@[simp]

theorem Filter.iInf_principal_finset {α : Type u} {ι : Type w} (s : Finset ι) (f : ι → Set α) : ⨅ i ∈ s, principal (f i) = principal (⋂ i ∈ s, f i)

theorem Filter.iInf_principal {α : Type u} {ι : Sort w} [Finite ι] (f : ι → Set α) : ⨅ (i : ι), principal (f i) = principal (⋂ (i : ι), f i)

@[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.

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)

Eventually and Frequently

@[simp]

theorem Filter.eventually_all {α : Type u} {ι : Sort u_2} [Finite ι] {l : Filter α} {p : ι → α → Prop} : (∀ᶠ (x : α) in l, ∀ (i : ι), p i x) ↔ ∀ (i : ι), ∀ᶠ (x : α) in l, p i x

@[simp]

theorem Filter.eventually_all_finite {α : Type u} {ι : Type u_2} {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

theorem Set.Finite.eventually_all {α : Type u} {ι : Type u_2} {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.

@[simp]

theorem Filter.eventually_all_finset {α : Type u} {ι : Type u_2} (I : Finset ι) {l : Filter α} {p : ι → α → Prop} : (∀ᶠ (x : α) in l, ∀ i ∈ I, p i x) ↔ ∀ i ∈ I, ∀ᶠ (x : α) in l, p i x

theorem Finset.eventually_all {α : Type u} {ι : Type u_2} (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.

@[simp]

theorem Filter.frequently_exists {α : Type u} {ι : Sort u_2} [Finite ι] {l : Filter α} {p : ι → α → Prop} : (∃ᶠ (x : α) in l, ∃ (i : ι), p i x) ↔ ∃ (i : ι), ∃ᶠ (x : α) in l, p i x

@[simp]

theorem Filter.frequently_exists_finite {α : Type u} {ι : Type u_2} {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

theorem Set.Finite.frequently_exists {α : Type u} {ι : Type u_2} {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.

@[simp]

theorem Filter.frequently_exists_finset {α : Type u} {ι : Type u_2} (I : Finset ι) {l : Filter α} {p : ι → α → Prop} : (∃ᶠ (x : α) in l, ∃ i ∈ I, p i x) ↔ ∃ i ∈ I, ∃ᶠ (x : α) in l, p i x

theorem Finset.frequently_exists {α : Type u} {ι : Type u_2} (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.

theorem Filter.eventually_subset_of_finite {α : Type u} {ι : Type u_2} {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”

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

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

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

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

theorem Set.Finite.eventuallyLE_iUnion {α : Type u} {l : Filter α} {ι : Type u_2} {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

theorem Filter.EventuallyLE.biUnion {α : Type u} {l : Filter α} {ι : Type u_2} {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.eventuallyLE_iUnion.

theorem Set.Finite.eventuallyEq_iUnion {α : Type u} {l : Filter α} {ι : Type u_2} {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

theorem Filter.EventuallyEq.biUnion {α : Type u} {l : Filter α} {ι : Type u_2} {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.eventuallyEq_iUnion.

theorem Set.Finite.eventuallyLE_iInter {α : Type u} {l : Filter α} {ι : Type u_2} {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

theorem Filter.EventuallyLE.biInter {α : Type u} {l : Filter α} {ι : Type u_2} {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.eventuallyLE_iInter.

theorem Set.Finite.eventuallyEq_iInter {α : Type u} {l : Filter α} {ι : Type u_2} {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

theorem Filter.EventuallyEq.biInter {α : Type u} {l : Filter α} {ι : Type u_2} {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.eventuallyEq_iInter.

theorem Finset.eventuallyLE_iUnion {α : Type u} {l : Filter α} {ι : Type u_2} (s : Finset ι) {f g : ι → Set α} (hle : ∀ i ∈ s, f i ≤ᶠ[l] g i) : ⋃ i ∈ s, f i ≤ᶠ[l] ⋃ i ∈ s, g i

theorem Finset.eventuallyEq_iUnion {α : Type u} {l : Filter α} {ι : Type u_2} (s : Finset ι) {f g : ι → Set α} (heq : ∀ i ∈ s, f i =ᶠ[l] g i) : ⋃ i ∈ s, f i =ᶠ[l] ⋃ i ∈ s, g i

theorem Finset.eventuallyLE_iInter {α : Type u} {l : Filter α} {ι : Type u_2} (s : Finset ι) {f g : ι → Set α} (hle : ∀ i ∈ s, f i ≤ᶠ[l] g i) : ⋂ i ∈ s, f i ≤ᶠ[l] ⋂ i ∈ s, g i

theorem Finset.eventuallyEq_iInter {α : Type u} {l : Filter α} {ι : Type u_2} (s : Finset ι) {f g : ι → Set α} (heq : ∀ i ∈ s, f i =ᶠ[l] g i) : ⋂ i ∈ s, f i =ᶠ[l] ⋂ i ∈ s, g i