# Theory of filters on sets #

A filter on a type `α` is a collection of sets of `α` which contains the whole `α`, is upwards-closed, and is stable under intersection. They are mostly used to abstract two related kinds of ideas:

- limits, including finite or infinite limits of sequences, finite or infinite limits of functions at a point or at infinity, etc...
- things happening eventually, including things happening for large enough `n : ℕ`, or near enough a point `x`, or for close enough pairs of points, or things happening almost everywhere in the sense of measure theory. Dually, filters can also express the idea of things happening often: for arbitrarily large `n`, or at a point in any neighborhood of given a point etc...

## Main definitions #

In this file, we endow `Filter α` it with a complete lattice structure. This structure is lifted from the lattice structure on `Set (Set X)` using the Galois insertion which maps a filter to its elements in one direction, and an arbitrary set of sets to the smallest filter containing it in the other direction. We also prove `Filter` is a monadic functor, with a push-forward operation `Filter.map` and a pull-back operation `Filter.comap` that form a Galois connections for the order on filters.

The examples of filters appearing in the description of the two motivating ideas are:

- `(Filter.atTop : Filter ℕ)` : made of sets of `ℕ` containing `{n | n ≥ N}` for some `N`
- `𝓝 x` : made of neighborhoods of `x` in a topological space (defined in topology.basic)
- `𝓤 X` : made of entourages of a uniform space (those space are generalizations of metric spaces defined in `Mathlib/Topology/UniformSpace/Basic.lean`)
- `MeasureTheory.ae` : made of sets whose complement has zero measure with respect to `μ` (defined in `Mathlib/MeasureTheory/OuterMeasure/AE`)

The predicate "happening eventually" is `Filter.Eventually`, and "happening often" is `Filter.Frequently`, whose definitions are immediate after `Filter` is defined (but they come rather late in this file in order to immediately relate them to the lattice structure).

## Notation #

- `∀ᶠ x in f, p x` : `f.Eventually p`;
- `∃ᶠ x in f, p x` : `f.Frequently p`;
- `f =ᶠ[l] g` : `∀ᶠ x in l, f x = g x`;
- `f ≤ᶠ[l] g` : `∀ᶠ x in l, f x ≤ g x`;
- `𝓟 s` : `Filter.Principal s`, localized in `Filter`.

## References #

- [N. Bourbaki, General Topology][bourbaki1966]

Important note: Bourbaki requires that a filter on `X` cannot contain all sets of `X`, which we do not require. This gives `Filter X` better formal properties, in particular a bottom element `⊥` for its lattice structure, at the cost of including the assumption `[NeBot f]` in a number of lemmas and definitions.

source
instance Filter.inhabitedMem {α : Type u} {f : Filter α} :
Inhabited { s : Set α // s ∈ f }
Equations

- Filter.inhabitedMem = { default := ⟨Set.univ, ⋯⟩ }

source
theorem Filter.filter_eq_iff {α : Type u} {f g : Filter α} :
f = g ↔ f.sets = g.sets
source
@[simp]
theorem Filter.sets_subset_sets {α : Type u} {f g : Filter α} :
f.sets ⊆ g.sets ↔ g ≤ f
source
@[simp]
theorem Filter.sets_ssubset_sets {α : Type u} {f g : Filter α} :
f.sets ⊂ g.sets ↔ g < f
source
theorem Filter.coext {α : Type u} {f g : Filter α} (h : ∀ (s : Set α), s ᶜ ∈ f ↔ s ᶜ ∈ g) :
f = g

An extensionality lemma that is useful for filters with good lemmas about `sᶜ ∈ f` (e.g., `Filter.comap`, `Filter.coprod`, `Filter.Coprod`, `Filter.cofinite`).

source
instance Filter.instTransSetSupersetMem {α : Type u} :
Trans (fun (x1 x2 : Set α) => x1 ⊇ x2) (fun (x1 : Set α) (x2 : Filter α) => x1 ∈ x2) fun (x1 : Set α) (x2 : Filter α) => x1 ∈ x2
Equations

- Filter.instTransSetSupersetMem = { trans := ⋯ }

source
instance Filter.instTransSetMemSubset {α : Type u} :
Trans Membership.mem (fun (x1 x2 : Set α) => x1 ⊆ x2) Membership.mem
Equations

- Filter.instTransSetMemSubset = { trans := ⋯ }

source
@[simp]
theorem Filter.inter_mem_iff {α : Type u} {f : Filter α} {s t : Set α} :
s ∩ t ∈ f ↔ s ∈ f ∧ t ∈ f
source
theorem Filter.diff_mem {α : Type u} {f : Filter α} {s t : Set α} (hs : s ∈ f) (ht : t ᶜ ∈ f) :
s \ t ∈ f
source
theorem Filter.congr_sets {α : Type u} {f : Filter α} {s t : Set α} (h : {x : α | x ∈ s ↔ x ∈ t} ∈ f) :
s ∈ f ↔ t ∈ f
source
theorem Filter.copy_eq {α : Type u} {f : Filter α} {S : Set (Set α)} (hmem : ∀ (s : Set α), s ∈ S ↔ s ∈ f) :
f.copy S hmem = f
source
theorem Filter.biInter_mem' {α : Type u} {f : Filter α} {β : Type v} {s : β → Set α} {is : Set β} (hf : is.Subsingleton) :
⋂ i ∈ is, s i ∈ f ↔ ∀ i ∈ is, s i ∈ f

Weaker version of `Filter.biInter_mem` that assumes `Subsingleton β` rather than `Finite β`.

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

Weaker version of `Filter.iInter_mem` that assumes `Subsingleton β` rather than `Finite β`.

source
theorem Filter.exists_mem_subset_iff {α : Type u} {f : Filter α} {s : Set α} :
(∃ t ∈ f, t ⊆ s) ↔ s ∈ f
source
theorem Filter.monotone_mem {α : Type u} {f : Filter α} :
Monotone fun (s : Set α) => s ∈ f
source
theorem Filter.exists_mem_and_iff {α : Type u} {f : Filter α} {P Q : Set α → Prop} (hP : Antitone P) (hQ : Antitone Q) :
((∃ u ∈ f, P u) ∧ ∃ u ∈ f, Q u) ↔ ∃ u ∈ f, P u ∧ Q u
source
@[deprecated forall_swap (since := "2025-06-10")]
theorem Filter.forall_in_swap {α : Type u} {f : Filter α} {β : Type u_1} {p : Set α → β → Prop} :
(∀ a ∈ f, ∀ (b : β), p a b) ↔ ∀ (b : β), ∀ a ∈ f, p a b
source
theorem Filter.mem_principal_self {α : Type u} (s : Set α) :
s ∈ principal s
source
theorem Filter.eventually_mem_principal {α : Type u} (s : Set α) :
∀ᶠ (x : α) in principal s, x ∈ s
source
theorem Filter.not_le {α : Type u} {f g : Filter α} :
¬f ≤ g ↔ ∃ s ∈ g, s ∉ f
source
inductive Filter.GenerateSets {α : Type u} (g : Set (Set α)) :
Set α → Prop

`GenerateSets g s`: `s` is in the filter closure of `g`.

- basic {α : Type u} {g : Set (Set α)} {s : Set α} : s ∈ g → GenerateSets g s
- univ {α : Type u} {g : Set (Set α)} : GenerateSets g Set.univ
- superset {α : Type u} {g : Set (Set α)} {s t : Set α} : GenerateSets g s → s ⊆ t → GenerateSets g t
- inter {α : Type u} {g : Set (Set α)} {s t : Set α} : GenerateSets g s → GenerateSets g t → GenerateSets g (s ∩ t)

Instances For

source
def Filter.generate {α : Type u} (g : Set (Set α)) :
Filter α

`generate g` is the largest filter containing the sets `g`.

Equations

- Filter.generate g = { sets := {s : Set α | Filter.GenerateSets g s}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

Instances For

source
theorem Filter.mem_generate_of_mem {α : Type u} {s : Set (Set α)} {U : Set α} (h : U ∈ s) :
U ∈ generate s
source
theorem Filter.le_generate_iff {α : Type u} {s : Set (Set α)} {f : Filter α} :
f ≤ generate s ↔ s ⊆ f.sets
source
@[simp]
theorem Filter.generate_singleton {α : Type u} (s : Set α) :
generate {s} = principal s
source
def Filter.mkOfClosure {α : Type u} (s : Set (Set α)) (hs : (generate s).sets = s) :
Filter α

`mkOfClosure s hs` constructs a filter on `α` whose elements set is exactly `s : Set (Set α)`, provided one gives the assumption `hs : (generate s).sets = s`.

Equations

- Filter.mkOfClosure s hs = { sets := s, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

Instances For

source
theorem Filter.mkOfClosure_sets {α : Type u} {s : Set (Set α)} {hs : (generate s).sets = s} :
Filter.mkOfClosure s hs = generate s
source
def Filter.giGenerate (α : Type u_2) :
GaloisInsertion generate sets

Galois insertion from sets of sets into filters.

Equations

- Filter.giGenerate α = { choice := fun (s : Set (Set α)) (hs : (Filter.generate s).sets ≤ s) => Filter.mkOfClosure s ⋯, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }

Instances For

source
theorem Filter.mem_inf_iff {α : Type u} {f g : Filter α} {s : Set α} :
s ∈ f ⊓ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, s = t₁ ∩ t₂
source
theorem Filter.mem_inf_of_left {α : Type u} {f g : Filter α} {s : Set α} (h : s ∈ f) :
s ∈ f ⊓ g
source
theorem Filter.mem_inf_of_right {α : Type u} {f g : Filter α} {s : Set α} (h : s ∈ g) :
s ∈ f ⊓ g
source
theorem Filter.inter_mem_inf {α : Type u} {f g : Filter α} {s t : Set α} (hs : s ∈ f) (ht : t ∈ g) :
s ∩ t ∈ f ⊓ g
source
theorem Filter.mem_inf_of_inter {α : Type u} {f g : Filter α} {s t u : Set α} (hs : s ∈ f) (ht : t ∈ g) (h : s ∩ t ⊆ u) :
u ∈ f ⊓ g
source
theorem Filter.mem_inf_iff_superset {α : Type u} {f g : Filter α} {s : Set α} :
s ∈ f ⊓ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ∩ t₂ ⊆ s
source
instance Filter.instCompleteLatticeFilter {α : Type u} :
CompleteLattice (Filter α)

Complete lattice structure on `Filter α`.

Equations

- One or more equations did not get rendered due to their size.

source
instance Filter.instInhabited {α : Type u} :
Inhabited (Filter α)
Equations

- Filter.instInhabited = { default := ⊥ }

source
theorem Filter.NeBot.ne {α : Type u} {f : Filter α} (hf : f.NeBot) :
f ≠ ⊥
source
@[simp]
theorem Filter.not_neBot {α : Type u} {f : Filter α} :
¬f.NeBot ↔ f = ⊥
source
theorem Filter.NeBot.mono {α : Type u} {f g : Filter α} (hf : f.NeBot) (hg : f ≤ g) :
g.NeBot
source
theorem Filter.neBot_of_le {α : Type u} {f g : Filter α} [hf : f.NeBot] (hg : f ≤ g) :
g.NeBot
source
@[simp]
theorem Filter.sup_neBot {α : Type u} {f g : Filter α} :
(f ⊔ g).NeBot ↔ f.NeBot ∨ g.NeBot
source
theorem Filter.not_disjoint_self_iff {α : Type u} {f : Filter α} :
¬Disjoint f f ↔ f.NeBot
source
theorem Filter.bot_sets_eq {α : Type u} :
⊥.sets = Set.univ
source
theorem Filter.eq_or_neBot {α : Type u} (f : Filter α) :
f = ⊥ ∨ f.NeBot

Either `f = ⊥` or `Filter.NeBot f`. This is a version of `eq_or_ne` that uses `Filter.NeBot` as the second alternative, to be used as an instance.

source
theorem Filter.sup_sets_eq {α : Type u} {f g : Filter α} :
(f ⊔ g).sets = f.sets ∩ g.sets
source
theorem Filter.sSup_sets_eq {α : Type u} {s : Set (Filter α)} :
(sSup s).sets = ⋂ f ∈ s, f.sets
source
theorem Filter.iSup_sets_eq {α : Type u} {ι : Sort x} {f : ι → Filter α} :
(iSup f).sets = ⋂ (i : ι), (f i).sets
source
theorem Filter.generate_empty {α : Type u} :
generate ∅ = ⊤
source
theorem Filter.generate_univ {α : Type u} :
generate Set.univ = ⊥
source
theorem Filter.generate_union {α : Type u} {s t : Set (Set α)} :
generate (s ∪ t) = generate s ⊓ generate t
source
theorem Filter.generate_iUnion {α : Type u} {ι : Sort x} {s : ι → Set (Set α)} :
generate (⋃ (i : ι), s i) = ⨅ (i : ι), generate (s i)
source
@[simp]
theorem Filter.mem_sup {α : Type u} {f g : Filter α} {s : Set α} :
s ∈ f ⊔ g ↔ s ∈ f ∧ s ∈ g
source
theorem Filter.union_mem_sup {α : Type u} {f g : Filter α} {s t : Set α} (hs : s ∈ f) (ht : t ∈ g) :
s ∪ t ∈ f ⊔ g
source
@[simp]
theorem Filter.mem_iSup {α : Type u} {ι : Sort x} {x : Set α} {f : ι → Filter α} :
x ∈ iSup f ↔ ∀ (i : ι), x ∈ f i
source
@[simp]
theorem Filter.iSup_neBot {α : Type u} {ι : Sort x} {f : ι → Filter α} :
(⨆ (i : ι), f i).NeBot ↔ ∃ (i : ι), (f i).NeBot
source
theorem Filter.iInf_eq_generate {α : Type u} {ι : Sort x} (s : ι → Filter α) :
iInf s = generate (⋃ (i : ι), (s i).sets)
source
theorem Filter.mem_iInf_of_mem {α : Type u} {ι : Sort x} {f : ι → Filter α} (i : ι) {s : Set α} (hs : s ∈ f i) :
s ∈ ⨅ (i : ι), f i
source
@[simp]
theorem Filter.le_principal_iff {α : Type u} {s : Set α} {f : Filter α} :
f ≤ principal s ↔ s ∈ f
source
theorem Filter.Iic_principal {α : Type u} (s : Set α) :
Set.Iic (principal s) = {l : Filter α | s ∈ l}
source
theorem Filter.principal_mono {α : Type u} {s t : Set α} :
principal s ≤ principal t ↔ s ⊆ t
source
theorem GCongr.filter_principal_mono {α : Type u} {s t : Set α} :
s ⊆ t → Filter.principal s ≤ Filter.principal t

Alias of the reverse direction of `Filter.principal_mono`.

source
theorem Filter.monotone_principal {α : Type u} :
Monotone principal
source
@[simp]
theorem Filter.principal_eq_iff_eq {α : Type u} {s t : Set α} :
principal s = principal t ↔ s = t
source
@[simp]
theorem Filter.join_principal_eq_sSup {α : Type u} {s : Set (Filter α)} :
(principal s).join = sSup s
source
@[simp]
theorem Filter.principal_univ {α : Type u} :
principal Set.univ = ⊤
source
@[simp]
theorem Filter.principal_empty {α : Type u} :
principal ∅ = ⊥
source
theorem Filter.generate_eq_biInf {α : Type u} (S : Set (Set α)) :
generate S = ⨅ s ∈ S, principal s

### Lattice equations #

source
theorem Filter.empty_mem_iff_bot {α : Type u} {f : Filter α} :
∅ ∈ f ↔ f = ⊥
source
theorem Filter.nonempty_of_mem {α : Type u} {f : Filter α} [hf : f.NeBot] {s : Set α} (hs : s ∈ f) :
s.Nonempty
source
theorem Filter.NeBot.nonempty_of_mem {α : Type u} {f : Filter α} (hf : f.NeBot) {s : Set α} (hs : s ∈ f) :
s.Nonempty
source
@[simp]
theorem Filter.empty_notMem {α : Type u} (f : Filter α) [f.NeBot] :
∅ ∉ f
source
@[deprecated Filter.empty_notMem (since := "2025-05-23")]
theorem Filter.empty_not_mem {α : Type u} (f : Filter α) [f.NeBot] :
∅ ∉ f

Alias of `Filter.empty_notMem`.

source
theorem Filter.nonempty_of_neBot {α : Type u} (f : Filter α) [f.NeBot] :
Nonempty α
source
theorem Filter.compl_notMem {α : Type u} {f : Filter α} {s : Set α} [f.NeBot] (h : s ∈ f) :
s ᶜ ∉ f
source
@[deprecated Filter.compl_notMem (since := "2025-05-23")]
theorem Filter.compl_not_mem {α : Type u} {f : Filter α} {s : Set α} [f.NeBot] (h : s ∈ f) :
s ᶜ ∉ f

Alias of `Filter.compl_notMem`.

source
theorem Filter.filter_eq_bot_of_isEmpty {α : Type u} [IsEmpty α] (f : Filter α) :
f = ⊥
source
theorem Filter.disjoint_iff {α : Type u} {f g : Filter α} :
Disjoint f g ↔ ∃ s ∈ f, ∃ t ∈ g, Disjoint s t
source
theorem Filter.disjoint_of_disjoint_of_mem {α : Type u} {f g : Filter α} {s t : Set α} (h : Disjoint s t) (hs : s ∈ f) (ht : t ∈ g) :
Disjoint f g
source
theorem Filter.NeBot.not_disjoint {α : Type u} {f : Filter α} {s t : Set α} (hf : f.NeBot) (hs : s ∈ f) (ht : t ∈ f) :
¬Disjoint s t
source
theorem Filter.inf_eq_bot_iff {α : Type u} {f g : Filter α} :
f ⊓ g = ⊥ ↔ ∃ U ∈ f, ∃ V ∈ g, U ∩ V = ∅
source
instance Filter.unique {α : Type u} [IsEmpty α] :
Unique (Filter α)

There is exactly one filter on an empty type.

Equations

- Filter.unique = { default := ⊥, uniq := ⋯ }

source
theorem Filter.NeBot.nonempty {α : Type u} (f : Filter α) [hf : f.NeBot] :
Nonempty α
source
theorem Filter.eq_top_of_neBot {α : Type u} [Subsingleton α] (l : Filter α) [l.NeBot] :
l = ⊤

There are only two filters on a `Subsingleton`: `⊥` and `⊤`. If the type is empty, then they are equal.

source
theorem Filter.forall_mem_nonempty_iff_neBot {α : Type u} {f : Filter α} :
(∀ s ∈ f, s.Nonempty) ↔ f.NeBot
source
instance Filter.instNeBotTop {α : Type u} [Nonempty α] :
⊤.NeBot
source
instance Filter.instNontrivialFilter {α : Type u} [Nonempty α] :
Nontrivial (Filter α)
source
theorem Filter.nontrivial_iff_nonempty {α : Type u} :
Nontrivial (Filter α) ↔ Nonempty α
source
theorem Filter.eq_sInf_of_mem_iff_exists_mem {α : Type u} {S : Set (Filter α)} {l : Filter α} (h : ∀ {s : Set α}, s ∈ l ↔ ∃ f ∈ S, s ∈ f) :
l = sInf S
source
theorem Filter.eq_iInf_of_mem_iff_exists_mem {α : Type u} {ι : Sort x} {f : ι → Filter α} {l : Filter α} (h : ∀ {s : Set α}, s ∈ l ↔ ∃ (i : ι), s ∈ f i) :
l = iInf f
source
theorem Filter.eq_biInf_of_mem_iff_exists_mem {α : Type u} {ι : Sort x} {f : ι → Filter α} {p : ι → Prop} {l : Filter α} (h : ∀ {s : Set α}, s ∈ l ↔ ∃ (i : ι), p i ∧ s ∈ f i) :
l = ⨅ (i : ι), ⨅ (_ : p i), f i
source
theorem Filter.iInf_sets_eq {α : Type u} {ι : Sort x} {f : ι → Filter α} (h : Directed (fun (x1 x2 : Filter α) => x1 ≥ x2) f) [ne : Nonempty ι] :
(iInf f).sets = ⋃ (i : ι), (f i).sets
source
theorem Filter.mem_iInf_of_directed {α : Type u} {ι : Sort x} {f : ι → Filter α} (h : Directed (fun (x1 x2 : Filter α) => x1 ≥ x2) f) [Nonempty ι] (s : Set α) :
s ∈ iInf f ↔ ∃ (i : ι), s ∈ f i
source
theorem Filter.mem_biInf_of_directed {α : Type u} {β : Type v} {f : β → Filter α} {s : Set β} (h : DirectedOn (f ⁻¹'o fun (x1 x2 : Filter α) => x1 ≥ x2) s) (ne : s.Nonempty) {t : Set α} :
t ∈ ⨅ i ∈ s, f i ↔ ∃ i ∈ s, t ∈ f i
source
theorem Filter.biInf_sets_eq {α : Type u} {β : Type v} {f : β → Filter α} {s : Set β} (h : DirectedOn (f ⁻¹'o fun (x1 x2 : Filter α) => x1 ≥ x2) s) (ne : s.Nonempty) :
(⨅ i ∈ s, f i).sets = ⋃ i ∈ s, (f i).sets
source
@[simp]
theorem Filter.sup_join {α : Type u} {f₁ f₂ : Filter (Filter α)} :
f₁.join ⊔ f₂.join = (f₁ ⊔ f₂).join
source
@[simp]
theorem Filter.iSup_join {α : Type u} {ι : Sort w} {f : ι → Filter (Filter α)} :
⨆ (x : ι), (f x).join = (⨆ (x : ι), f x).join
source
instance Filter.instDistribLattice {α : Type u} :
DistribLattice (Filter α)
Equations

- Filter.instDistribLattice = { toLattice := Filter.instCompleteLatticeFilter.toLattice, le_sup_inf := ⋯ }

source
theorem Filter.iInf_neBot_of_directed' {α : Type u} {ι : Sort x} {f : ι → Filter α} [Nonempty ι] (hd : Directed (fun (x1 x2 : Filter α) => x1 ≥ x2) f) :
(∀ (i : ι), (f i).NeBot) → (iInf f).NeBot

If `f : ι → Filter α` is directed, `ι` is not empty, and `∀ i, f i ≠ ⊥`, then `iInf f ≠ ⊥`. See also `iInf_neBot_of_directed` for a version assuming `Nonempty α` instead of `Nonempty ι`.

source
theorem Filter.iInf_neBot_of_directed {α : Type u} {ι : Sort x} {f : ι → Filter α} [hn : Nonempty α] (hd : Directed (fun (x1 x2 : Filter α) => x1 ≥ x2) f) (hb : ∀ (i : ι), (f i).NeBot) :
(iInf f).NeBot

If `f : ι → Filter α` is directed, `α` is not empty, and `∀ i, f i ≠ ⊥`, then `iInf f ≠ ⊥`. See also `iInf_neBot_of_directed'` for a version assuming `Nonempty ι` instead of `Nonempty α`.

source
theorem Filter.sInf_neBot_of_directed' {α : Type u} {s : Set (Filter α)} (hne : s.Nonempty) (hd : DirectedOn (fun (x1 x2 : Filter α) => x1 ≥ x2) s) (hbot : ⊥ ∉ s) :
(sInf s).NeBot
source
theorem Filter.sInf_neBot_of_directed {α : Type u} [Nonempty α] {s : Set (Filter α)} (hd : DirectedOn (fun (x1 x2 : Filter α) => x1 ≥ x2) s) (hbot : ⊥ ∉ s) :
(sInf s).NeBot
source
theorem Filter.iInf_neBot_iff_of_directed' {α : Type u} {ι : Sort x} {f : ι → Filter α} [Nonempty ι] (hd : Directed (fun (x1 x2 : Filter α) => x1 ≥ x2) f) :
(iInf f).NeBot ↔ ∀ (i : ι), (f i).NeBot
source
theorem Filter.iInf_neBot_iff_of_directed {α : Type u} {ι : Sort x} {f : ι → Filter α} [Nonempty α] (hd : Directed (fun (x1 x2 : Filter α) => x1 ≥ x2) f) :
(iInf f).NeBot ↔ ∀ (i : ι), (f i).NeBot

#### `principal` equations #

source
@[simp]
theorem Filter.inf_principal {α : Type u} {s t : Set α} :
principal s ⊓ principal t = principal (s ∩ t)
source
@[simp]
theorem Filter.sup_principal {α : Type u} {s t : Set α} :
principal s ⊔ principal t = principal (s ∪ t)
source
@[simp]
theorem Filter.iSup_principal {α : Type u} {ι : Sort w} {s : ι → Set α} :
⨆ (x : ι), principal (s x) = principal (⋃ (i : ι), s i)
source
@[simp]
theorem Filter.principal_eq_bot_iff {α : Type u} {s : Set α} :
principal s = ⊥ ↔ s = ∅
source
@[simp]
theorem Filter.principal_neBot_iff {α : Type u} {s : Set α} :
(principal s).NeBot ↔ s.Nonempty
source
theorem Set.Nonempty.principal_neBot {α : Type u} {s : Set α} :
s.Nonempty → (Filter.principal s).NeBot

Alias of the reverse direction of `Filter.principal_neBot_iff`.

source
theorem Filter.isCompl_principal {α : Type u} (s : Set α) :
IsCompl (principal s) (principal s ᶜ)
source
theorem Filter.mem_inf_principal' {α : Type u} {f : Filter α} {s t : Set α} :
s ∈ f ⊓ principal t ↔ t ᶜ ∪ s ∈ f
source
theorem Filter.mem_inf_principal {α : Type u} {f : Filter α} {s t : Set α} :
s ∈ f ⊓ principal t ↔ {x : α | x ∈ t → x ∈ s} ∈ f
source
theorem Filter.iSup_inf_principal {α : Type u} {ι : Sort x} (f : ι → Filter α) (s : Set α) :
⨆ (i : ι), f i ⊓ principal s = (⨆ (i : ι), f i) ⊓ principal s
source
theorem Filter.inf_principal_eq_bot {α : Type u} {f : Filter α} {s : Set α} :
f ⊓ principal s = ⊥ ↔ s ᶜ ∈ f
source
theorem Filter.mem_of_eq_bot {α : Type u} {f : Filter α} {s : Set α} (h : f ⊓ principal s ᶜ = ⊥) :
s ∈ f
source
theorem Filter.diff_mem_inf_principal_compl {α : Type u} {f : Filter α} {s : Set α} (hs : s ∈ f) (t : Set α) :
s \ t ∈ f ⊓ principal t ᶜ
source
theorem Filter.principal_le_iff {α : Type u} {s : Set α} {f : Filter α} :
principal s ≤ f ↔ ∀ V ∈ f, s ⊆ V
source
theorem Filter.join_mono {α : Type u} {f₁ f₂ : Filter (Filter α)} (h : f₁ ≤ f₂) :
f₁.join ≤ f₂.join

### Eventually #

source
theorem Filter.eventually_iff {α : Type u} {f : Filter α} {P : α → Prop} :
(∀ᶠ (x : α) in f, P x) ↔ {x : α | P x} ∈ f
source
@[simp]
theorem Filter.eventually_mem_set {α : Type u} {s : Set α} {l : Filter α} :
(∀ᶠ (x : α) in l, x ∈ s) ↔ s ∈ l
source
theorem Filter.ext' {α : Type u} {f₁ f₂ : Filter α} (h : ∀ (p : α → Prop), (∀ᶠ (x : α) in f₁, p x) ↔ ∀ᶠ (x : α) in f₂, p x) :
f₁ = f₂
source
theorem Filter.Eventually.filter_mono {α : Type u} {f₁ f₂ : Filter α} (h : f₁ ≤ f₂) {p : α → Prop} (hp : ∀ᶠ (x : α) in f₂, p x) :
∀ᶠ (x : α) in f₁, p x
source
theorem Filter.eventually_of_mem {α : Type u} {f : Filter α} {P : α → Prop} {U : Set α} (hU : U ∈ f) (h : ∀ x ∈ U, P x) :
∀ᶠ (x : α) in f, P x
source
theorem Filter.Eventually.and {α : Type u} {p q : α → Prop} {f : Filter α} :
Filter.Eventually p f → Filter.Eventually q f → ∀ᶠ (x : α) in f, p x ∧ q x
source
@[simp]
theorem Filter.eventually_true {α : Type u} (f : Filter α) :
∀ᶠ (x : α) in f, True
source
theorem Filter.Eventually.of_forall {α : Type u} {p : α → Prop} {f : Filter α} (hp : ∀ (x : α), p x) :
∀ᶠ (x : α) in f, p x
source
@[simp]
theorem Filter.eventually_false_iff_eq_bot {α : Type u} {f : Filter α} :
(∀ᶠ (x : α) in f, False) ↔ f = ⊥
source
@[simp]
theorem Filter.eventually_const {α : Type u} {f : Filter α} [t : f.NeBot] {p : Prop} :
(∀ᶠ (x : α) in f, p) ↔ p
source
theorem Filter.eventually_iff_exists_mem {α : Type u} {p : α → Prop} {f : Filter α} :
(∀ᶠ (x : α) in f, p x) ↔ ∃ v ∈ f, ∀ y ∈ v, p y
source
theorem Filter.Eventually.exists_mem {α : Type u} {p : α → Prop} {f : Filter α} (hp : ∀ᶠ (x : α) in f, p x) :
∃ v ∈ f, ∀ y ∈ v, p y
source
theorem Filter.Eventually.mp {α : Type u} {p q : α → Prop} {f : Filter α} (hp : ∀ᶠ (x : α) in f, p x) (hq : ∀ᶠ (x : α) in f, p x → q x) :
∀ᶠ (x : α) in f, q x
source
theorem Filter.Eventually.mono {α : Type u} {p q : α → Prop} {f : Filter α} (hp : ∀ᶠ (x : α) in f, p x) (hq : ∀ (x : α), p x → q x) :
∀ᶠ (x : α) in f, q x
source
theorem Filter.GCongr.eventually_mono {α : Type u} {p q : α → Prop} {f : Filter α} (h : ∀ (x : α), p x → q x) :
(∀ᶠ (x : α) in f, p x) → ∀ᶠ (x : α) in f, q x
source
theorem Filter.forall_eventually_of_eventually_forall {α : Type u} {β : Type v} {f : Filter α} {p : α → β → Prop} (h : ∀ᶠ (x : α) in f, ∀ (y : β), p x y) (y : β) :
∀ᶠ (x : α) in f, p x y
source
@[simp]
theorem Filter.eventually_and {α : Type u} {p q : α → Prop} {f : Filter α} :
(∀ᶠ (x : α) in f, p x ∧ q x) ↔ (∀ᶠ (x : α) in f, p x) ∧ ∀ᶠ (x : α) in f, q x
source
theorem Filter.Eventually.congr {α : Type u} {f : Filter α} {p q : α → Prop} (h' : ∀ᶠ (x : α) in f, p x) (h : ∀ᶠ (x : α) in f, p x ↔ q x) :
∀ᶠ (x : α) in f, q x
source
theorem Filter.eventually_congr {α : Type u} {f : Filter α} {p q : α → Prop} (h : ∀ᶠ (x : α) in f, p x ↔ q x) :
(∀ᶠ (x : α) in f, p x) ↔ ∀ᶠ (x : α) in f, q x
source
@[simp]
theorem Filter.eventually_or_distrib_left {α : Type u} {f : Filter α} {p : Prop} {q : α → Prop} :
(∀ᶠ (x : α) in f, p ∨ q x) ↔ p ∨ ∀ᶠ (x : α) in f, q x
source
@[simp]
theorem Filter.eventually_or_distrib_right {α : Type u} {f : Filter α} {p : α → Prop} {q : Prop} :
(∀ᶠ (x : α) in f, p x ∨ q) ↔ (∀ᶠ (x : α) in f, p x) ∨ q
source
theorem Filter.eventually_imp_distrib_left {α : Type u} {f : Filter α} {p : Prop} {q : α → Prop} :
(∀ᶠ (x : α) in f, p → q x) ↔ p → ∀ᶠ (x : α) in f, q x
source
@[simp]
theorem Filter.eventually_bot {α : Type u} {p : α → Prop} :
∀ᶠ (x : α) in ⊥, p x
source
@[simp]
theorem Filter.eventually_top {α : Type u} {p : α → Prop} :
(∀ᶠ (x : α) in ⊤, p x) ↔ ∀ (x : α), p x
source
@[simp]
theorem Filter.eventually_sup {α : Type u} {p : α → Prop} {f g : Filter α} :
(∀ᶠ (x : α) in f ⊔ g, p x) ↔ (∀ᶠ (x : α) in f, p x) ∧ ∀ᶠ (x : α) in g, p x
source
@[simp]
theorem Filter.eventually_sSup {α : Type u} {p : α → Prop} {fs : Set (Filter α)} :
(∀ᶠ (x : α) in sSup fs, p x) ↔ ∀ f ∈ fs, ∀ᶠ (x : α) in f, p x
source
@[simp]
theorem Filter.eventually_iSup {α : Type u} {ι : Sort x} {p : α → Prop} {fs : ι → Filter α} :
(∀ᶠ (x : α) in ⨆ (b : ι), fs b, p x) ↔ ∀ (b : ι), ∀ᶠ (x : α) in fs b, p x
source
@[simp]
theorem Filter.eventually_principal {α : Type u} {a : Set α} {p : α → Prop} :
(∀ᶠ (x : α) in principal a, p x) ↔ ∀ x ∈ a, p x
source
theorem Filter.Eventually.forall_mem {α : Type u_2} {f : Filter α} {s : Set α} {P : α → Prop} (hP : ∀ᶠ (x : α) in f, P x) (hf : principal s ≤ f) (x : α) :
x ∈ s → P x
source
theorem Filter.eventually_inf {α : Type u} {f g : Filter α} {p : α → Prop} :
(∀ᶠ (x : α) in f ⊓ g, p x) ↔ ∃ s ∈ f, ∃ t ∈ g, ∀ x ∈ s ∩ t, p x
source
theorem Filter.eventually_inf_principal {α : Type u} {f : Filter α} {p : α → Prop} {s : Set α} :
(∀ᶠ (x : α) in f ⊓ principal s, p x) ↔ ∀ᶠ (x : α) in f, x ∈ s → p x
source
theorem Filter.eventually_iff_all_subsets {α : Type u} {f : Filter α} {p : α → Prop} :
(∀ᶠ (x : α) in f, p x) ↔ ∀ (s : Set α), ∀ᶠ (x : α) in f, x ∈ s → p x

### Frequently #

source
theorem Filter.Eventually.frequently {α : Type u} {f : Filter α} [f.NeBot] {p : α → Prop} (h : ∀ᶠ (x : α) in f, p x) :
∃ᶠ (x : α) in f, p x
source
theorem Filter.Frequently.of_forall {α : Type u} {f : Filter α} [f.NeBot] {p : α → Prop} (h : ∀ (x : α), p x) :
∃ᶠ (x : α) in f, p x
source
theorem Filter.Frequently.mp {α : Type u} {p q : α → Prop} {f : Filter α} (h : ∃ᶠ (x : α) in f, p x) (hpq : ∀ᶠ (x : α) in f, p x → q x) :
∃ᶠ (x : α) in f, q x
source
theorem Filter.frequently_congr {α : Type u} {p q : α → Prop} {f : Filter α} (h : ∀ᶠ (x : α) in f, p x ↔ q x) :
(∃ᶠ (x : α) in f, p x) ↔ ∃ᶠ (x : α) in f, q x
source
theorem Filter.Frequently.filter_mono {α : Type u} {p : α → Prop} {f g : Filter α} (h : ∃ᶠ (x : α) in f, p x) (hle : f ≤ g) :
∃ᶠ (x : α) in g, p x
source
theorem Filter.Frequently.mono {α : Type u} {p q : α → Prop} {f : Filter α} (h : ∃ᶠ (x : α) in f, p x) (hpq : ∀ (x : α), p x → q x) :
∃ᶠ (x : α) in f, q x
source
theorem Filter.GCongr.frequently_mono {α : Type u} {p q : α → Prop} {f : Filter α} (h : ∀ (x : α), p x → q x) :
(∃ᶠ (x : α) in f, p x) → ∃ᶠ (x : α) in f, q x
source
theorem Filter.Frequently.and_eventually {α : Type u} {p q : α → Prop} {f : Filter α} (hp : ∃ᶠ (x : α) in f, p x) (hq : ∀ᶠ (x : α) in f, q x) :
∃ᶠ (x : α) in f, p x ∧ q x
source
theorem Filter.Eventually.and_frequently {α : Type u} {p q : α → Prop} {f : Filter α} (hp : ∀ᶠ (x : α) in f, p x) (hq : ∃ᶠ (x : α) in f, q x) :
∃ᶠ (x : α) in f, p x ∧ q x
source
theorem Filter.Frequently.exists {α : Type u} {p : α → Prop} {f : Filter α} (hp : ∃ᶠ (x : α) in f, p x) :
∃ (x : α), p x
source
theorem Filter.Eventually.exists {α : Type u} {p : α → Prop} {f : Filter α} [f.NeBot] (hp : ∀ᶠ (x : α) in f, p x) :
∃ (x : α), p x
source
theorem Filter.frequently_iff_neBot {α : Type u} {l : Filter α} {p : α → Prop} :
(∃ᶠ (x : α) in l, p x) ↔ (l ⊓ principal {x : α | p x}).NeBot
source
theorem Filter.frequently_mem_iff_neBot {α : Type u} {l : Filter α} {s : Set α} :
(∃ᶠ (x : α) in l, x ∈ s) ↔ (l ⊓ principal s).NeBot
source
theorem Filter.frequently_iff_forall_eventually_exists_and {α : Type u} {p : α → Prop} {f : Filter α} :
(∃ᶠ (x : α) in f, p x) ↔ ∀ {q : α → Prop}, (∀ᶠ (x : α) in f, q x) → ∃ (x : α), p x ∧ q x
source
theorem Filter.frequently_iff {α : Type u} {f : Filter α} {P : α → Prop} :
(∃ᶠ (x : α) in f, P x) ↔ ∀ {U : Set α}, U ∈ f → ∃ x ∈ U, P x
source
@[simp]
theorem Filter.not_eventually {α : Type u} {p : α → Prop} {f : Filter α} :
(¬∀ᶠ (x : α) in f, p x) ↔ ∃ᶠ (x : α) in f, ¬p x
source
@[simp]
theorem Filter.not_frequently {α : Type u} {p : α → Prop} {f : Filter α} :
(¬∃ᶠ (x : α) in f, p x) ↔ ∀ᶠ (x : α) in f, ¬p x
source
@[simp]
theorem Filter.frequently_true_iff_neBot {α : Type u} (f : Filter α) :
(∃ᶠ (x : α) in f, True) ↔ f.NeBot
source
@[simp]
theorem Filter.frequently_false {α : Type u} (f : Filter α) :
¬∃ᶠ (x : α) in f, False
source
@[simp]
theorem Filter.frequently_const {α : Type u} {f : Filter α} [f.NeBot] {p : Prop} :
(∃ᶠ (x : α) in f, p) ↔ p
source
@[simp]
theorem Filter.frequently_or_distrib {α : Type u} {f : Filter α} {p q : α → Prop} :
(∃ᶠ (x : α) in f, p x ∨ q x) ↔ (∃ᶠ (x : α) in f, p x) ∨ ∃ᶠ (x : α) in f, q x
source
theorem Filter.frequently_or_distrib_left {α : Type u} {f : Filter α} [f.NeBot] {p : Prop} {q : α → Prop} :
(∃ᶠ (x : α) in f, p ∨ q x) ↔ p ∨ ∃ᶠ (x : α) in f, q x
source
theorem Filter.frequently_or_distrib_right {α : Type u} {f : Filter α} [f.NeBot] {p : α → Prop} {q : Prop} :
(∃ᶠ (x : α) in f, p x ∨ q) ↔ (∃ᶠ (x : α) in f, p x) ∨ q
source
theorem Filter.frequently_imp_distrib {α : Type u} {f : Filter α} {p q : α → Prop} :
(∃ᶠ (x : α) in f, p x → q x) ↔ (∀ᶠ (x : α) in f, p x) → ∃ᶠ (x : α) in f, q x
source
theorem Filter.frequently_imp_distrib_left {α : Type u} {f : Filter α} [f.NeBot] {p : Prop} {q : α → Prop} :
(∃ᶠ (x : α) in f, p → q x) ↔ p → ∃ᶠ (x : α) in f, q x
source
theorem Filter.frequently_imp_distrib_right {α : Type u} {f : Filter α} [f.NeBot] {p : α → Prop} {q : Prop} :
(∃ᶠ (x : α) in f, p x → q) ↔ (∀ᶠ (x : α) in f, p x) → q
source
theorem Filter.eventually_imp_distrib_right {α : Type u} {f : Filter α} {p : α → Prop} {q : Prop} :
(∀ᶠ (x : α) in f, p x → q) ↔ (∃ᶠ (x : α) in f, p x) → q
source
@[simp]
theorem Filter.frequently_and_distrib_left {α : Type u} {f : Filter α} {p : Prop} {q : α → Prop} :
(∃ᶠ (x : α) in f, p ∧ q x) ↔ p ∧ ∃ᶠ (x : α) in f, q x
source
@[simp]
theorem Filter.frequently_and_distrib_right {α : Type u} {f : Filter α} {p : α → Prop} {q : Prop} :
(∃ᶠ (x : α) in f, p x ∧ q) ↔ (∃ᶠ (x : α) in f, p x) ∧ q
source
@[simp]
theorem Filter.frequently_bot {α : Type u} {p : α → Prop} :
¬∃ᶠ (x : α) in ⊥, p x
source
@[simp]
theorem Filter.frequently_top {α : Type u} {p : α → Prop} :
(∃ᶠ (x : α) in ⊤, p x) ↔ ∃ (x : α), p x
source
@[simp]
theorem Filter.frequently_principal {α : Type u} {a : Set α} {p : α → Prop} :
(∃ᶠ (x : α) in principal a, p x) ↔ ∃ x ∈ a, p x
source
theorem Filter.frequently_inf_principal {α : Type u} {f : Filter α} {s : Set α} {p : α → Prop} :
(∃ᶠ (x : α) in f ⊓ principal s, p x) ↔ ∃ᶠ (x : α) in f, x ∈ s ∧ p x
source
theorem Filter.Frequently.of_inf_principal {α : Type u} {f : Filter α} {s : Set α} {p : α → Prop} :
(∃ᶠ (x : α) in f ⊓ principal s, p x) → ∃ᶠ (x : α) in f, x ∈ s ∧ p x

Alias of the forward direction of `Filter.frequently_inf_principal`.

source
theorem Filter.Frequently.inf_principal {α : Type u} {f : Filter α} {s : Set α} {p : α → Prop} :
(∃ᶠ (x : α) in f, x ∈ s ∧ p x) → ∃ᶠ (x : α) in f ⊓ principal s, p x

Alias of the reverse direction of `Filter.frequently_inf_principal`.

source
theorem Filter.frequently_sup {α : Type u} {p : α → Prop} {f g : Filter α} :
(∃ᶠ (x : α) in f ⊔ g, p x) ↔ (∃ᶠ (x : α) in f, p x) ∨ ∃ᶠ (x : α) in g, p x
source
@[simp]
theorem Filter.frequently_sSup {α : Type u} {p : α → Prop} {fs : Set (Filter α)} :
(∃ᶠ (x : α) in sSup fs, p x) ↔ ∃ f ∈ fs, ∃ᶠ (x : α) in f, p x
source
@[simp]
theorem Filter.frequently_iSup {α : Type u} {β : Type v} {p : α → Prop} {fs : β → Filter α} :
(∃ᶠ (x : α) in ⨆ (b : β), fs b, p x) ↔ ∃ (b : β), ∃ᶠ (x : α) in fs b, p x
source
theorem Filter.Eventually.choice {α : Type u} {β : Type v} {r : α → β → Prop} {l : Filter α} [l.NeBot] (h : ∀ᶠ (x : α) in l, ∃ (y : β), r x y) :
∃ (f : α → β), ∀ᶠ (x : α) in l, r x (f x)
source
theorem Filter.skolem {ι : Type u_2} {α : ι → Type u_3} [∀ (i : ι), Nonempty (α i)] {P : (i : ι) → α i → Prop} {F : Filter ι} :
(∀ᶠ (i : ι) in F, ∃ (b : α i), P i b) ↔ ∃ (b : (i : ι) → α i), ∀ᶠ (i : ι) in F, P i (b i)

### Relation “eventually equal” #

source
theorem Filter.EventuallyEq.eventually {α : Type u} {β : Type v} {l : Filter α} {f g : α → β} (h : f =ᶠ[l] g) :
∀ᶠ (x : α) in l, f x = g x
source
@[simp]
theorem Filter.eventuallyEq_top {α : Type u} {β : Type v} {f g : α → β} :
f =ᶠ[⊤] g ↔ f = g
source
theorem Filter.EventuallyEq.rw {α : Type u} {β : Type v} {l : Filter α} {f g : α → β} (h : f =ᶠ[l] g) (p : α → β → Prop) (hf : ∀ᶠ (x : α) in l, p x (f x)) :
∀ᶠ (x : α) in l, p x (g x)
source
theorem Filter.eventuallyEq_set {α : Type u} {s t : Set α} {l : Filter α} :
s =ᶠ[l] t ↔ ∀ᶠ (x : α) in l, x ∈ s ↔ x ∈ t
source
theorem Filter.Eventually.set_eq {α : Type u} {s t : Set α} {l : Filter α} :
(∀ᶠ (x : α) in l, x ∈ s ↔ x ∈ t) → s =ᶠ[l] t

Alias of the reverse direction of `Filter.eventuallyEq_set`.

source
theorem Filter.EventuallyEq.mem_iff {α : Type u} {s t : Set α} {l : Filter α} :
s =ᶠ[l] t → ∀ᶠ (x : α) in l, x ∈ s ↔ x ∈ t

Alias of the forward direction of `Filter.eventuallyEq_set`.

source
@[simp]
theorem Filter.eventuallyEq_univ {α : Type u} {s : Set α} {l : Filter α} :
s =ᶠ[l] Set.univ ↔ s ∈ l
source
theorem Filter.EventuallyEq.exists_mem {α : Type u} {β : Type v} {l : Filter α} {f g : α → β} (h : f =ᶠ[l] g) :
∃ s ∈ l, Set.EqOn f g s
source
theorem Filter.eventuallyEq_of_mem {α : Type u} {β : Type v} {l : Filter α} {f g : α → β} {s : Set α} (hs : s ∈ l) (h : Set.EqOn f g s) :
f =ᶠ[l] g
source
theorem Filter.eventuallyEq_iff_exists_mem {α : Type u} {β : Type v} {l : Filter α} {f g : α → β} :
f =ᶠ[l] g ↔ ∃ s ∈ l, Set.EqOn f g s
source
theorem Filter.EventuallyEq.filter_mono {α : Type u} {β : Type v} {l l' : Filter α} {f g : α → β} (h₁ : f =ᶠ[l] g) (h₂ : l' ≤ l) :
f =ᶠ[l'] g
source
@[simp]
theorem Filter.EventuallyEq.refl {α : Type u} {β : Type v} (l : Filter α) (f : α → β) :
f =ᶠ[l] f
source
theorem Filter.EventuallyEq.rfl {α : Type u} {β : Type v} {l : Filter α} {f : α → β} :
f =ᶠ[l] f
source
theorem Filter.EventuallyEq.of_eq {α : Type u} {β : Type v} {l : Filter α} {f g : α → β} (h : f = g) :
f =ᶠ[l] g
source
theorem Eq.eventuallyEq {α : Type u} {β : Type v} {l : Filter α} {f g : α → β} (h : f = g) :
f =ᶠ[l] g

Alias of `Filter.EventuallyEq.of_eq`.

source
theorem Filter.EventuallyEq.symm {α : Type u} {β : Type v} {f g : α → β} {l : Filter α} (H : f =ᶠ[l] g) :
g =ᶠ[l] f
source
theorem Filter.eventuallyEq_comm {α : Type u} {β : Type v} {f g : α → β} {l : Filter α} :
f =ᶠ[l] g ↔ g =ᶠ[l] f
source
theorem Filter.EventuallyEq.trans {α : Type u} {β : Type v} {l : Filter α} {f g h : α → β} (H₁ : f =ᶠ[l] g) (H₂ : g =ᶠ[l] h) :
f =ᶠ[l] h
source
theorem Filter.EventuallyEq.congr_left {α : Type u} {β : Type v} {l : Filter α} {f g h : α → β} (H : f =ᶠ[l] g) :
f =ᶠ[l] h ↔ g =ᶠ[l] h
source
theorem Filter.EventuallyEq.congr_right {α : Type u} {β : Type v} {l : Filter α} {f g h : α → β} (H : g =ᶠ[l] h) :
f =ᶠ[l] g ↔ f =ᶠ[l] h
source
instance Filter.instTransForallEventuallyEq {α : Type u} {β : Type v} {l : Filter α} :
Trans (fun (x1 x2 : α → β) => x1 =ᶠ[l] x2) (fun (x1 x2 : α → β) => x1 =ᶠ[l] x2) fun (x1 x2 : α → β) => x1 =ᶠ[l] x2
Equations

- Filter.instTransForallEventuallyEq = { trans := ⋯ }

source
theorem Filter.EventuallyEq.prodMk {α : Type u} {β : Type v} {γ : Type w} {l : Filter α} {f f' : α → β} (hf : f =ᶠ[l] f') {g g' : α → γ} (hg : g =ᶠ[l] g') :
(fun (x : α) => (f x, g x)) =ᶠ[l] fun (x : α) => (f' x, g' x)
source
theorem Filter.EventuallyEq.fun_comp {α : Type u} {β : Type v} {γ : Type w} {f g : α → β} {l : Filter α} (H : f =ᶠ[l] g) (h : β → γ) :
h ∘ f =ᶠ[l] h ∘ g
source
theorem Filter.EventuallyEq.comp₂ {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_2} {f f' : α → β} {g g' : α → γ} {l : Filter α} (Hf : f =ᶠ[l] f') (h : β → γ → δ) (Hg : g =ᶠ[l] g') :
(fun (x : α) => h (f x) (g x)) =ᶠ[l] fun (x : α) => h (f' x) (g' x)
source
theorem Filter.EventuallyEq.mul {α : Type u} {β : Type v} [Mul β] {f f' g g' : α → β} {l : Filter α} (h : f =ᶠ[l] g) (h' : f' =ᶠ[l] g') :
f * f' =ᶠ[l] g * g'
source
theorem Filter.EventuallyEq.add {α : Type u} {β : Type v} [Add β] {f f' g g' : α → β} {l : Filter α} (h : f =ᶠ[l] g) (h' : f' =ᶠ[l] g') :
f + f' =ᶠ[l] g + g'
source
theorem Filter.EventuallyEq.fun_mul {α : Type u} {β : Type v} [Mul β] {f f' g g' : α → β} {l : Filter α} (h : f =ᶠ[l] g) (h' : f' =ᶠ[l] g') :
(fun (x : α) => f x * f' x) =ᶠ[l] fun (x : α) => g x * g' x
source
theorem Filter.EventuallyEq.fun_add {α : Type u} {β : Type v} [Add β] {f f' g g' : α → β} {l : Filter α} (h : f =ᶠ[l] g) (h' : f' =ᶠ[l] g') :
(fun (x : α) => f x + f' x) =ᶠ[l] fun (x : α) => g x + g' x
source
theorem Filter.EventuallyEq.mul_left {α : Type u} {β : Type v} {l : Filter α} [Mul β] {f₁ f₂ f₃ : α → β} (h : f₁ =ᶠ[l] f₂) :
f₃ * f₁ =ᶠ[l] f₃ * f₂
source
theorem Filter.EventuallyEq.add_left {α : Type u} {β : Type v} {l : Filter α} [Add β] {f₁ f₂ f₃ : α → β} (h : f₁ =ᶠ[l] f₂) :
f₃ + f₁ =ᶠ[l] f₃ + f₂
source
theorem Filter.EventuallyEq.mul_right {α : Type u} {β : Type v} {l : Filter α} [Mul β] {f₁ f₂ f₃ : α → β} (h : f₁ =ᶠ[l] f₂) :
f₁ * f₃ =ᶠ[l] f₂ * f₃
source
theorem Filter.EventuallyEq.add_right {α : Type u} {β : Type v} {l : Filter α} [Add β] {f₁ f₂ f₃ : α → β} (h : f₁ =ᶠ[l] f₂) :
f₁ + f₃ =ᶠ[l] f₂ + f₃
source
theorem Filter.EventuallyEq.pow_const {α : Type u} {β : Type v} {γ : Type u_2} [Pow β γ] {f g : α → β} {l : Filter α} (h : f =ᶠ[l] g) (c : γ) :
f ^ c =ᶠ[l] g ^ c
source
theorem Filter.EventuallyEq.const_vadd {α : Type u} {β : Type v} {γ : Type u_2} [VAdd γ β] {f g : α → β} {l : Filter α} (h : f =ᶠ[l] g) (c : γ) :
c +ᵥ f =ᶠ[l] c +ᵥ g
source
theorem Filter.EventuallyEq.const_smul {α : Type u} {β : Type v} {γ : Type u_2} [SMul γ β] {f g : α → β} {l : Filter α} (h : f =ᶠ[l] g) (c : γ) :
c • f =ᶠ[l] c • g
source
theorem Filter.EventuallyEq.fun_pow_const {α : Type u} {β : Type v} {γ : Type u_2} [Pow β γ] {f g : α → β} {l : Filter α} (h : f =ᶠ[l] g) (c : γ) :
(fun (x : α) => f x ^ c) =ᶠ[l] fun (x : α) => g x ^ c
source
theorem Filter.EventuallyEq.fun_const_smul {α : Type u} {β : Type v} {γ : Type u_2} [SMul γ β] {f g : α → β} {l : Filter α} (h : f =ᶠ[l] g) (c : γ) :
(fun (x : α) => c • f x) =ᶠ[l] fun (x : α) => c • g x
source
theorem Filter.EventuallyEq.fun_const_vadd {α : Type u} {β : Type v} {γ : Type u_2} [VAdd γ β] {f g : α → β} {l : Filter α} (h : f =ᶠ[l] g) (c : γ) :
(fun (x : α) => c +ᵥ f x) =ᶠ[l] fun (x : α) => c +ᵥ g x
source
theorem Filter.EventuallyEq.inv {α : Type u} {β : Type v} [Inv β] {f g : α → β} {l : Filter α} (h : f =ᶠ[l] g) :
f⁻¹ =ᶠ[l] g⁻¹
source
theorem Filter.EventuallyEq.neg {α : Type u} {β : Type v} [Neg β] {f g : α → β} {l : Filter α} (h : f =ᶠ[l] g) :
-f =ᶠ[l] -g
source
theorem Filter.EventuallyEq.fun_inv {α : Type u} {β : Type v} [Inv β] {f g : α → β} {l : Filter α} (h : f =ᶠ[l] g) :
(fun (x : α) => (f x)⁻¹) =ᶠ[l] fun (x : α) => (g x)⁻¹
source
theorem Filter.EventuallyEq.fun_neg {α : Type u} {β : Type v} [Neg β] {f g : α → β} {l : Filter α} (h : f =ᶠ[l] g) :
(fun (x : α) => -f x) =ᶠ[l] fun (x : α) => -g x
source
theorem Filter.EventuallyEq.div {α : Type u} {β : Type v} [Div β] {f f' g g' : α → β} {l : Filter α} (h : f =ᶠ[l] g) (h' : f' =ᶠ[l] g') :
f / f' =ᶠ[l] g / g'
source
theorem Filter.EventuallyEq.sub {α : Type u} {β : Type v} [Sub β] {f f' g g' : α → β} {l : Filter α} (h : f =ᶠ[l] g) (h' : f' =ᶠ[l] g') :
f - f' =ᶠ[l] g - g'
source
theorem Filter.EventuallyEq.fun_div {α : Type u} {β : Type v} [Div β] {f f' g g' : α → β} {l : Filter α} (h : f =ᶠ[l] g) (h' : f' =ᶠ[l] g') :
(fun (x : α) => f x / f' x) =ᶠ[l] fun (x : α) => g x / g' x
source
theorem Filter.EventuallyEq.fun_sub {α : Type u} {β : Type v} [Sub β] {f f' g g' : α → β} {l : Filter α} (h : f =ᶠ[l] g) (h' : f' =ᶠ[l] g') :
(fun (x : α) => f x - f' x) =ᶠ[l] fun (x : α) => g x - g' x
source
theorem Filter.EventuallyEq.smul {α : Type u} {β : Type v} {𝕜 : Type u_2} [SMul 𝕜 β] {l : Filter α} {f f' : α → 𝕜} {g g' : α → β} (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') :
(fun (x : α) => f x • g x) =ᶠ[l] fun (x : α) => f' x • g' x
source
theorem Filter.EventuallyEq.vadd {α : Type u} {β : Type v} {𝕜 : Type u_2} [VAdd 𝕜 β] {l : Filter α} {f f' : α → 𝕜} {g g' : α → β} (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') :
(fun (x : α) => f x +ᵥ g x) =ᶠ[l] fun (x : α) => f' x +ᵥ g' x
source
theorem Filter.EventuallyEq.fun_star {α : Type u} {R : Type u_2} [Star R] {f g : α → R} {l : Filter α} (h : f =ᶠ[l] g) :
(fun (x : α) => star (f x)) =ᶠ[l] fun (x : α) => star (g x)
source
theorem Filter.EventuallyEq.star {α : Type u} {R : Type u_2} [Star R] {f g : α → R} {l : Filter α} (h : f =ᶠ[l] g) :
star f =ᶠ[l] star g
source
theorem Filter.EventuallyEq.sup {α : Type u} {β : Type v} [Max β] {l : Filter α} {f f' g g' : α → β} (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') :
f ⊔ g =ᶠ[l] f' ⊔ g'
source
theorem Filter.EventuallyEq.inf {α : Type u} {β : Type v} [Min β] {l : Filter α} {f f' g g' : α → β} (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') :
f ⊓ g =ᶠ[l] f' ⊓ g'
source
theorem Filter.EventuallyEq.preimage {α : Type u} {β : Type v} {l : Filter α} {f g : α → β} (h : f =ᶠ[l] g) (s : Set β) :
f ⁻¹' s =ᶠ[l] g ⁻¹' s
source
theorem Filter.EventuallyEq.inter {α : Type u} {s t s' t' : Set α} {l : Filter α} (h : s =ᶠ[l] t) (h' : s' =ᶠ[l] t') :
s ∩ s' =ᶠ[l] t ∩ t'
source
theorem Filter.EventuallyEq.union {α : Type u} {s t s' t' : Set α} {l : Filter α} (h : s =ᶠ[l] t) (h' : s' =ᶠ[l] t') :
s ∪ s' =ᶠ[l] t ∪ t'
source
theorem Filter.EventuallyEq.compl {α : Type u} {s t : Set α} {l : Filter α} (h : s =ᶠ[l] t) :
s ᶜ =ᶠ[l] t ᶜ
source
theorem Filter.EventuallyEq.diff {α : Type u} {s t s' t' : Set α} {l : Filter α} (h : s =ᶠ[l] t) (h' : s' =ᶠ[l] t') :
s \ s' =ᶠ[l] t \ t'
source
theorem Filter.EventuallyEq.symmDiff {α : Type u} {s t s' t' : Set α} {l : Filter α} (h : s =ᶠ[l] t) (h' : s' =ᶠ[l] t') :
symmDiff s s' =ᶠ[l] symmDiff t t'
source
theorem Filter.eventuallyEq_empty {α : Type u} {s : Set α} {l : Filter α} :
s =ᶠ[l] ∅ ↔ ∀ᶠ (x : α) in l, x ∉ s
source
theorem Filter.inter_eventuallyEq_left {α : Type u} {s t : Set α} {l : Filter α} :
s ∩ t =ᶠ[l] s ↔ ∀ᶠ (x : α) in l, x ∈ s → x ∈ t
source
theorem Filter.inter_eventuallyEq_right {α : Type u} {s t : Set α} {l : Filter α} :
s ∩ t =ᶠ[l] t ↔ ∀ᶠ (x : α) in l, x ∈ t → x ∈ s
source
@[simp]
theorem Filter.eventuallyEq_principal {α : Type u} {β : Type v} {s : Set α} {f g : α → β} :
f =ᶠ[principal s] g ↔ Set.EqOn f g s
source
theorem Filter.eventuallyEq_inf_principal_iff {α : Type u} {β : Type v} {F : Filter α} {s : Set α} {f g : α → β} :
f =ᶠ[F ⊓ principal s] g ↔ ∀ᶠ (x : α) in F, x ∈ s → f x = g x
source
theorem Filter.EventuallyEq.sub_eq {α : Type u} {β : Type v} [AddGroup β] {f g : α → β} {l : Filter α} (h : f =ᶠ[l] g) :
f - g =ᶠ[l] 0
source
theorem Filter.eventuallyEq_iff_sub {α : Type u} {β : Type v} [AddGroup β] {f g : α → β} {l : Filter α} :
f =ᶠ[l] g ↔ f - g =ᶠ[l] 0
source
theorem Filter.eventuallyEq_iff_all_subsets {α : Type u} {β : Type v} {f g : α → β} {l : Filter α} :
f =ᶠ[l] g ↔ ∀ (s : Set α), ∀ᶠ (x : α) in l, x ∈ s → f x = g x
source
theorem Filter.EventuallyLE.congr {α : Type u} {β : Type v} [LE β] {l : Filter α} {f f' g g' : α → β} (H : f ≤ᶠ[l] g) (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') :
f' ≤ᶠ[l] g'
source
theorem Filter.eventuallyLE_congr {α : Type u} {β : Type v} [LE β] {l : Filter α} {f f' g g' : α → β} (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') :
f ≤ᶠ[l] g ↔ f' ≤ᶠ[l] g'
source
theorem Filter.eventuallyLE_iff_all_subsets {α : Type u} {β : Type v} [LE β] {f g : α → β} {l : Filter α} :
f ≤ᶠ[l] g ↔ ∀ (s : Set α), ∀ᶠ (x : α) in l, x ∈ s → f x ≤ g x
source
theorem Filter.EventuallyEq.le {α : Type u} {β : Type v} [Preorder β] {l : Filter α} {f g : α → β} (h : f =ᶠ[l] g) :
f ≤ᶠ[l] g
source
theorem Filter.EventuallyLE.refl {α : Type u} {β : Type v} [Preorder β] (l : Filter α) (f : α → β) :
f ≤ᶠ[l] f
source
theorem Filter.EventuallyLE.rfl {α : Type u} {β : Type v} [Preorder β] {l : Filter α} {f : α → β} :
f ≤ᶠ[l] f
source
theorem Filter.EventuallyLE.trans {α : Type u} {β : Type v} [Preorder β] {l : Filter α} {f g h : α → β} (H₁ : f ≤ᶠ[l] g) (H₂ : g ≤ᶠ[l] h) :
f ≤ᶠ[l] h
source
instance Filter.instTransForallEventuallyLE {α : Type u} {β : Type v} [Preorder β] {l : Filter α} :
Trans (fun (x1 x2 : α → β) => x1 ≤ᶠ[l] x2) (fun (x1 x2 : α → β) => x1 ≤ᶠ[l] x2) fun (x1 x2 : α → β) => x1 ≤ᶠ[l] x2
Equations

- Filter.instTransForallEventuallyLE = { trans := ⋯ }

source
theorem Filter.EventuallyEq.trans_le {α : Type u} {β : Type v} [Preorder β] {l : Filter α} {f g h : α → β} (H₁ : f =ᶠ[l] g) (H₂ : g ≤ᶠ[l] h) :
f ≤ᶠ[l] h
source
instance Filter.instTransForallEventuallyEqEventuallyLE {α : Type u} {β : Type v} [Preorder β] {l : Filter α} :
Trans (fun (x1 x2 : α → β) => x1 =ᶠ[l] x2) (fun (x1 x2 : α → β) => x1 ≤ᶠ[l] x2) fun (x1 x2 : α → β) => x1 ≤ᶠ[l] x2
Equations

- Filter.instTransForallEventuallyEqEventuallyLE = { trans := ⋯ }

source
theorem Filter.EventuallyLE.trans_eq {α : Type u} {β : Type v} [Preorder β] {l : Filter α} {f g h : α → β} (H₁ : f ≤ᶠ[l] g) (H₂ : g =ᶠ[l] h) :
f ≤ᶠ[l] h
source
instance Filter.instTransForallEventuallyLEEventuallyEq {α : Type u} {β : Type v} [Preorder β] {l : Filter α} :
Trans (fun (x1 x2 : α → β) => x1 ≤ᶠ[l] x2) (fun (x1 x2 : α → β) => x1 =ᶠ[l] x2) fun (x1 x2 : α → β) => x1 ≤ᶠ[l] x2
Equations

- Filter.instTransForallEventuallyLEEventuallyEq = { trans := ⋯ }

source
theorem Filter.EventuallyLE.antisymm {α : Type u} {β : Type v} [PartialOrder β] {l : Filter α} {f g : α → β} (h₁ : f ≤ᶠ[l] g) (h₂ : g ≤ᶠ[l] f) :
f =ᶠ[l] g
source
theorem Filter.eventuallyLE_antisymm_iff {α : Type u} {β : Type v} [PartialOrder β] {l : Filter α} {f g : α → β} :
f =ᶠ[l] g ↔ f ≤ᶠ[l] g ∧ g ≤ᶠ[l] f
source
theorem Filter.EventuallyLE.ge_iff_eq' {α : Type u} {β : Type v} [PartialOrder β] {l : Filter α} {f g : α → β} (h : f ≤ᶠ[l] g) :
g ≤ᶠ[l] f ↔ g =ᶠ[l] f
source
@[deprecated Filter.EventuallyLE.ge_iff_eq' (since := "2025-07-10")]
theorem Filter.EventuallyLE.le_iff_eq {α : Type u} {β : Type v} [PartialOrder β] {l : Filter α} {f g : α → β} (h : f ≤ᶠ[l] g) :
g ≤ᶠ[l] f ↔ g =ᶠ[l] f

Alias of `Filter.EventuallyLE.ge_iff_eq'`.

source
theorem Filter.Eventually.ne_of_lt {α : Type u} {β : Type v} [Preorder β] {l : Filter α} {f g : α → β} (h : ∀ᶠ (x : α) in l, f x < g x) :
∀ᶠ (x : α) in l, f x ≠ g x
source
theorem Filter.Eventually.ne_top_of_lt {α : Type u} {β : Type v} [Preorder β] [OrderTop β] {l : Filter α} {f g : α → β} (h : ∀ᶠ (x : α) in l, f x < g x) :
∀ᶠ (x : α) in l, f x ≠ ⊤
source
theorem Filter.Eventually.lt_top_of_ne {α : Type u} {β : Type v} [PartialOrder β] [OrderTop β] {l : Filter α} {f : α → β} (h : ∀ᶠ (x : α) in l, f x ≠ ⊤) :
∀ᶠ (x : α) in l, f x < ⊤
source
theorem Filter.Eventually.lt_top_iff_ne_top {α : Type u} {β : Type v} [PartialOrder β] [OrderTop β] {l : Filter α} {f : α → β} :
(∀ᶠ (x : α) in l, f x < ⊤) ↔ ∀ᶠ (x : α) in l, f x ≠ ⊤
source
theorem Filter.EventuallyLE.inter {α : Type u} {s t s' t' : Set α} {l : Filter α} (h : s ≤ᶠ[l] t) (h' : s' ≤ᶠ[l] t') :
s ∩ s' ≤ᶠ[l] t ∩ t'
source
theorem Filter.EventuallyLE.union {α : Type u} {s t s' t' : Set α} {l : Filter α} (h : s ≤ᶠ[l] t) (h' : s' ≤ᶠ[l] t') :
s ∪ s' ≤ᶠ[l] t ∪ t'
source
theorem Filter.EventuallyLE.compl {α : Type u} {s t : Set α} {l : Filter α} (h : s ≤ᶠ[l] t) :
t ᶜ ≤ᶠ[l] s ᶜ
source
theorem Filter.EventuallyLE.diff {α : Type u} {s t s' t' : Set α} {l : Filter α} (h : s ≤ᶠ[l] t) (h' : t' ≤ᶠ[l] s') :
s \ s' ≤ᶠ[l] t \ t'
source
theorem Filter.set_eventuallyLE_iff_mem_inf_principal {α : Type u} {s t : Set α} {l : Filter α} :
s ≤ᶠ[l] t ↔ t ∈ l ⊓ principal s
source
theorem Filter.set_eventuallyLE_iff_inf_principal_le {α : Type u} {s t : Set α} {l : Filter α} :
s ≤ᶠ[l] t ↔ l ⊓ principal s ≤ l ⊓ principal t
source
theorem Filter.set_eventuallyEq_iff_inf_principal {α : Type u} {s t : Set α} {l : Filter α} :
s =ᶠ[l] t ↔ l ⊓ principal s = l ⊓ principal t
source
theorem Filter.EventuallyLE.sup {α : Type u} {β : Type v} [SemilatticeSup β] {l : Filter α} {f₁ f₂ g₁ g₂ : α → β} (hf : f₁ ≤ᶠ[l] f₂) (hg : g₁ ≤ᶠ[l] g₂) :
f₁ ⊔ g₁ ≤ᶠ[l] f₂ ⊔ g₂
source
theorem Filter.EventuallyLE.sup_le {α : Type u} {β : Type v} [SemilatticeSup β] {l : Filter α} {f g h : α → β} (hf : f ≤ᶠ[l] h) (hg : g ≤ᶠ[l] h) :
f ⊔ g ≤ᶠ[l] h
source
theorem Filter.EventuallyLE.le_sup_of_le_left {α : Type u} {β : Type v} [SemilatticeSup β] {l : Filter α} {f g h : α → β} (hf : h ≤ᶠ[l] f) :
h ≤ᶠ[l] f ⊔ g
source
theorem Filter.EventuallyLE.le_sup_of_le_right {α : Type u} {β : Type v} [SemilatticeSup β] {l : Filter α} {f g h : α → β} (hg : h ≤ᶠ[l] g) :
h ≤ᶠ[l] f ⊔ g
source
theorem Filter.join_le {α : Type u} {f : Filter (Filter α)} {l : Filter α} (h : ∀ᶠ (m : Filter α) in f, m ≤ l) :
f.join ≤ l
source
theorem Set.EqOn.eventuallyEq {α : Type u_1} {β : Type u_2} {s : Set α} {f g : α → β} (h : EqOn f g s) :
f =ᶠ[Filter.principal s] g
source
theorem Set.EqOn.eventuallyEq_of_mem {α : Type u_1} {β : Type u_2} {s : Set α} {l : Filter α} {f g : α → β} (h : EqOn f g s) (hl : s ∈ l) :
f =ᶠ[l] g
source
theorem HasSubset.Subset.eventuallyLE {α : Type u_1} {l : Filter α} {s t : Set α} (h : s ⊆ t) :
s ≤ᶠ[l] t
source
theorem Filter.compl_mem_comk {α : Type u_1} {p : Set α → Prop} {he : p ∅} {hmono : ∀ (t : Set α), p t → ∀ s ⊆ t, p s} {hunion : ∀ (s : Set α), p s → ∀ (t : Set α), p t → p (s ∪ t)} {s : Set α} :
s ᶜ ∈ comk p he hmono hunion ↔ p s