# mathlib3documentation

order.filter.basic

# Theory of filters on sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

## Main definitions #

• `filter` : filters on a set;
• `at_top`, `at_bot`, `cofinite`, `principal` : specific filters;
• `map`, `comap` : operations on filters;
• `tendsto` : limit with respect to filters;
• `eventually` : `f.eventually p` means `{x | p x} ∈ f`;
• `frequently` : `f.frequently p` means `{x | ¬p x} ∉ f`;
• `filter_upwards [h₁, ..., hₙ]` : takes a list of proofs `hᵢ : sᵢ ∈ f`, and replaces a goal `s ∈ f` with `∀ x, x ∈ s₁ → ... → x ∈ sₙ → x ∈ s`;
• `ne_bot f` : an utility class stating that `f` is a non-trivial filter.

Filters on a type `X` are sets of sets of `X` satisfying three conditions. 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...

In this file, we define the type `filter X` of filters on `X`, and endow 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:

• `(at_top : 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 topology.uniform_space.basic)
• `μ.ae` : made of sets whose complement has zero measure with respect to `μ` (defined in `measure_theory.measure_space`)

The general notion of limit of a map with respect to filters on the source and target types is `filter.tendsto`. It is defined in terms of the order and the push-forward operation. 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).

For instance, anticipating on topology.basic, the statement: "if a sequence `u` converges to some `x` and `u n` belongs to a set `M` for `n` large enough then `x` is in the closure of `M`" is formalized as: `tendsto u at_top (𝓝 x) → (∀ᶠ n in at_top, u n ∈ M) → x ∈ closure M`, which is a special case of `mem_closure_of_tendsto` from topology.basic.

## Notations #

• `∀ᶠ 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` : `principal s`, localized in `filter`.

## References #

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 `[ne_bot f]` in a number of lemmas and definitions.

structure filter (α : Type u_1) :
Type u_1

A filter `F` on a type `α` is a collection of sets of `α` which contains the whole `α`, is upwards-closed, and is stable under intersection. We do not forbid this collection to be all sets of `α`.

Instances for `filter`
@[protected, instance]
def filter.has_mem {α : Type u_1} :
has_mem (set α) (filter α)

If `F` is a filter on `α`, and `U` a subset of `α` then we can write `U ∈ F` as on paper.

Equations
@[protected, simp]
theorem filter.mem_mk {α : Type u} {s : set α} {t : set (set α)} {h₁ : set.univ t} {h₂ : {x y : set α}, x t x y y t} {h₃ : {x y : set α}, x t y t x y t} :
s {sets := t, univ_sets := h₁, sets_of_superset := h₂, inter_sets := h₃} s t
@[protected, simp]
theorem filter.mem_sets {α : Type u} {f : filter α} {s : set α} :
s f.sets s f
@[protected, instance]
def filter.inhabited_mem {α : Type u} {f : filter α} :
inhabited {s // s f}
Equations
theorem filter.filter_eq {α : Type u} {f g : filter α} :
f.sets = g.sets f = g
theorem filter.filter_eq_iff {α : Type u} {f g : filter α} :
f = g f.sets = g.sets
@[protected]
theorem filter.ext_iff {α : Type u} {f g : filter α} :
f = g (s : set α), s f s g
@[protected, ext]
theorem filter.ext {α : Type u} {f g : filter α} :
( (s : set α), s f s g) f = g
@[protected]
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`).

@[simp]
theorem filter.univ_mem {α : Type u} {f : filter α} :
theorem filter.mem_of_superset {α : Type u} {f : filter α} {x y : set α} (hx : x f) (hxy : x y) :
y f
theorem filter.inter_mem {α : Type u} {f : filter α} {s t : set α} (hs : s f) (ht : t f) :
s t f
@[simp]
theorem filter.inter_mem_iff {α : Type u} {f : filter α} {s t : set α} :
s t f s f t f
theorem filter.diff_mem {α : Type u} {f : filter α} {s t : set α} (hs : s f) (ht : t f) :
s \ t f
theorem filter.univ_mem' {α : Type u} {f : filter α} {s : set α} (h : (a : α), a s) :
s f
theorem filter.mp_mem {α : Type u} {f : filter α} {s t : set α} (hs : s f) (h : {x : α | x s x t} f) :
t f
theorem filter.congr_sets {α : Type u} {f : filter α} {s t : set α} (h : {x : α | x s x t} f) :
s f t f
@[simp]
theorem filter.bInter_mem {α : Type u} {f : filter α} {β : Type v} {s : β set α} {is : set β} (hf : is.finite) :
( (i : β) (H : i is), s i) f (i : β), i is s i f
@[simp]
theorem filter.bInter_finset_mem {α : Type u} {f : filter α} {β : Type v} {s : β set α} (is : finset β) :
( (i : β) (H : i is), s i) f (i : β), i is s i f
@[protected]
theorem finset.Inter_mem_sets {α : Type u} {f : filter α} {β : Type v} {s : β set α} (is : finset β) :
( (i : β) (H : i is), s i) f (i : β), i is s i f

Alias of `filter.bInter_finset_mem`.

@[simp]
theorem filter.sInter_mem {α : Type u} {f : filter α} {s : set (set α)} (hfin : s.finite) :
⋂₀ s f (U : set α), U s U f
@[simp]
theorem filter.Inter_mem {α : Type u} {f : filter α} {β : Type v} {s : β set α} [finite β] :
( (i : β), s i) f (i : β), s i f
theorem filter.exists_mem_subset_iff {α : Type u} {f : filter α} {s : set α} :
( (t : set α) (H : t f), t s) s f
theorem filter.monotone_mem {α : Type u} {f : filter α} :
monotone (λ (s : set α), s f)
theorem filter.exists_mem_and_iff {α : Type u} {f : filter α} {P Q : set α Prop} (hP : antitone P) (hQ : antitone Q) :
(( (u : set α) (H : u f), P u) (u : set α) (H : u f), Q u) (u : set α) (H : u f), P u Q u
theorem filter.forall_in_swap {α : Type u} {f : filter α} {β : Type u_1} {p : set α β Prop} :
( (a : set α), a f (b : β), p a b) (b : β) (a : set α), a f p a b

`filter_upwards [h₁, ⋯, hₙ]` replaces a goal of the form `s ∈ f` and terms `h₁ : t₁ ∈ f, ⋯, hₙ : tₙ ∈ f` with `∀ x, x ∈ t₁ → ⋯ → x ∈ tₙ → x ∈ s`. The list is an optional parameter, `[]` being its default value.

`filter_upwards [h₁, ⋯, hₙ] with a₁ a₂ ⋯ aₖ` is a short form for `{ filter_upwards [h₁, ⋯, hₙ], intros a₁ a₂ ⋯ aₖ }`.

`filter_upwards [h₁, ⋯, hₙ] using e` is a short form for `{ filter_upwards [h1, ⋯, hn], exact e }`.

Combining both shortcuts is done by writing `filter_upwards [h₁, ⋯, hₙ] with a₁ a₂ ⋯ aₖ using e`. Note that in this case, the `aᵢ` terms can be used in `e`.

`filter_upwards [h₁, ⋯, hₙ]` replaces a goal of the form `s ∈ f` and terms `h₁ : t₁ ∈ f, ⋯, hₙ : tₙ ∈ f` with `∀ x, x ∈ t₁ → ⋯ → x ∈ tₙ → x ∈ s`. The list is an optional parameter, `[]` being its default value.

`filter_upwards [h₁, ⋯, hₙ] with a₁ a₂ ⋯ aₖ` is a short form for `{ filter_upwards [h₁, ⋯, hₙ], intros a₁ a₂ ⋯ aₖ }`.

`filter_upwards [h₁, ⋯, hₙ] using e` is a short form for `{ filter_upwards [h1, ⋯, hn], exact e }`.

Combining both shortcuts is done by writing `filter_upwards [h₁, ⋯, hₙ] with a₁ a₂ ⋯ aₖ using e`. Note that in this case, the `aᵢ` terms can be used in `e`.

def filter.principal {α : Type u} (s : set α) :

The principal filter of `s` is the collection of all supersets of `s`.

Equations
Instances for `filter.principal`
@[simp]
theorem filter.mem_principal {α : Type u} {s t : set α} :
t s
theorem filter.mem_principal_self {α : Type u} (s : set α) :
def filter.join {α : Type u} (f : filter (filter α)) :

The join of a filter of filters is defined by the relation `s ∈ join f ↔ {t | s ∈ t} ∈ f`.

Equations
@[simp]
theorem filter.mem_join {α : Type u} {s : set α} {f : filter (filter α)} :
s f.join {t : | s t} f
@[protected, instance]
def filter.partial_order {α : Type u} :
Equations
theorem filter.le_def {α : Type u} {f g : filter α} :
f g (x : set α), x g x f
@[protected]
theorem filter.not_le {α : Type u} {f g : filter α} :
¬f g (s : set α) (H : s g), s f
inductive filter.generate_sets {α : Type u} (g : set (set α)) :
set α Prop

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

def filter.generate {α : Type u} (g : set (set α)) :

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

Equations
theorem filter.sets_iff_generate {α : Type u} {s : set (set α)} {f : filter α} :
s f.sets
theorem filter.mem_generate_iff {α : Type u} {s : set (set α)} {U : set α} :
(t : set (set α)) (H : t s), t.finite ⋂₀ t U
@[protected]
def filter.mk_of_closure {α : Type u} (s : set (set α)) (hs : .sets = s) :

`mk_of_closure 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
theorem filter.mk_of_closure_sets {α : Type u} {s : set (set α)} {hs : .sets = s} :
def filter.gi_generate (α : Type u_1) :

Galois insertion from sets of sets into filters.

Equations
@[protected, instance]
def filter.has_inf {α : Type u} :

The infimum of filters is the filter generated by intersections of elements of the two filters.

Equations
theorem filter.mem_inf_iff {α : Type u} {f g : filter α} {s : set α} :
s f g (t₁ : set α) (H : t₁ f) (t₂ : set α) (H : t₂ g), s = t₁ t₂
theorem filter.mem_inf_of_left {α : Type u} {f g : filter α} {s : set α} (h : s f) :
s f g
theorem filter.mem_inf_of_right {α : Type u} {f g : filter α} {s : set α} (h : s g) :
s f g
theorem filter.inter_mem_inf {α : Type u} {f g : filter α} {s t : set α} (hs : s f) (ht : t g) :
s t f g
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
theorem filter.mem_inf_iff_superset {α : Type u} {f g : filter α} {s : set α} :
s f g (t₁ : set α) (H : t₁ f) (t₂ : set α) (H : t₂ g), t₁ t₂ s
@[protected, instance]
def filter.has_top {α : Type u} :
Equations
theorem filter.mem_top_iff_forall {α : Type u} {s : set α} :
s (x : α), x s
@[simp]
theorem filter.mem_top {α : Type u} {s : set α} :
@[protected, instance]
def filter.complete_lattice {α : Type u} :
Equations
@[protected, instance]
def filter.inhabited {α : Type u} :
Equations
@[class]
structure filter.ne_bot {α : Type u} (f : filter α) :
Prop

A filter is `ne_bot` if it is not equal to `⊥`, or equivalently the empty set does not belong to the filter. Bourbaki include this assumption in the definition of a filter but we prefer to have a `complete_lattice` structure on filter, so we use a typeclass argument in lemmas instead.

Instances of this typeclass
theorem filter.ne_bot_iff {α : Type u} {f : filter α} :
theorem filter.ne_bot.ne {α : Type u} {f : filter α} (hf : f.ne_bot) :
@[simp]
theorem filter.not_ne_bot {α : Type u_1} {f : filter α} :
theorem filter.ne_bot.mono {α : Type u} {f g : filter α} (hf : f.ne_bot) (hg : f g) :
theorem filter.ne_bot_of_le {α : Type u} {f g : filter α} [hf : f.ne_bot] (hg : f g) :
@[simp]
theorem filter.sup_ne_bot {α : Type u} {f g : filter α} :
theorem filter.not_disjoint_self_iff {α : Type u} {f : filter α} :
theorem filter.bot_sets_eq {α : Type u} :
theorem filter.sup_sets_eq {α : Type u} {f g : filter α} :
(f g).sets = f.sets g.sets
theorem filter.Sup_sets_eq {α : Type u} {s : set (filter α)} :
(has_Sup.Sup s).sets = (f : filter α) (H : f s), f.sets
theorem filter.supr_sets_eq {α : Type u} {ι : Sort x} {f : ι } :
(supr f).sets = (i : ι), (f i).sets
theorem filter.generate_empty {α : Type u} :
theorem filter.generate_univ {α : Type u} :
theorem filter.generate_union {α : Type u} {s t : set (set α)} :
theorem filter.generate_Union {α : Type u} {ι : Sort x} {s : ι set (set α)} :
filter.generate ( (i : ι), s i) = (i : ι), filter.generate (s i)
@[simp]
theorem filter.mem_bot {α : Type u} {s : set α} :
@[simp]
theorem filter.mem_sup {α : Type u} {f g : filter α} {s : set α} :
s f g s f s g
theorem filter.union_mem_sup {α : Type u} {f g : filter α} {s t : set α} (hs : s f) (ht : t g) :
s t f g
@[simp]
theorem filter.mem_Sup {α : Type u} {x : set α} {s : set (filter α)} :
x (f : filter α), f s x f
@[simp]
theorem filter.mem_supr {α : Type u} {ι : Sort x} {x : set α} {f : ι } :
x supr f (i : ι), x f i
@[simp]
theorem filter.supr_ne_bot {α : Type u} {ι : Sort x} {f : ι } :
( (i : ι), f i).ne_bot (i : ι), (f i).ne_bot
theorem filter.infi_eq_generate {α : Type u} {ι : Sort x} (s : ι ) :
infi s = filter.generate ( (i : ι), (s i).sets)
theorem filter.mem_infi_of_mem {α : Type u} {ι : Sort x} {f : ι } (i : ι) {s : set α} :
s f i (s (i : ι), f i)
theorem filter.mem_infi_of_Inter {α : Type u} {ι : Type u_1} {s : ι } {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_infi {α : Type u} {ι : Type u_1} {s : ι } {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_infi' {α : Type u} {ι : Type u_1} {s : ι } {U : set α} :
(U (i : ι), s i) (I : set ι), I.finite (V : ι set α), ( (i : ι), V i s i) ( (i : ι), i I V i = set.univ) (U = (i : ι) (H : i I), V i) U = (i : ι), V i
theorem filter.exists_Inter_of_mem_infi {ι : Type u_1} {α : Type u_2} {f : ι } {s : set α} (hs : s (i : ι), f i) :
(t : ι set α), ( (i : ι), t i f i) s = (i : ι), t i
theorem filter.mem_infi_of_finite {ι : Type u_1} [finite ι] {α : Type u_2} {f : ι } (s : set α) :
(s (i : ι), f i) (t : ι set α), ( (i : ι), t i f i) s = (i : ι), t i
@[simp]
theorem filter.le_principal_iff {α : Type u} {s : set α} {f : filter α} :
s f
theorem filter.Iic_principal {α : Type u} (s : set α) :
= {l : | s l}
theorem filter.principal_mono {α : Type u} {s t : set α} :
s t
theorem filter.monotone_principal {α : Type u} :
@[simp]
theorem filter.principal_eq_iff_eq {α : Type u} {s t : set α} :
s = t
@[simp]
theorem filter.join_principal_eq_Sup {α : Type u} {s : set (filter α)} :
@[simp]
theorem filter.principal_univ {α : Type u} :
@[simp]
theorem filter.principal_empty {α : Type u} :
theorem filter.generate_eq_binfi {α : Type u} (S : set (set α)) :
= (s : set α) (H : s S),

### Lattice equations #

theorem filter.empty_mem_iff_bot {α : Type u} {f : filter α} :
theorem filter.nonempty_of_mem {α : Type u} {f : filter α} [hf : f.ne_bot] {s : set α} (hs : s f) :
theorem filter.ne_bot.nonempty_of_mem {α : Type u} {f : filter α} (hf : f.ne_bot) {s : set α} (hs : s f) :
@[simp]
theorem filter.empty_not_mem {α : Type u} (f : filter α) [f.ne_bot] :
theorem filter.nonempty_of_ne_bot {α : Type u} (f : filter α) [f.ne_bot] :
theorem filter.compl_not_mem {α : Type u} {f : filter α} {s : set α} [f.ne_bot] (h : s f) :
s f
theorem filter.filter_eq_bot_of_is_empty {α : Type u} [is_empty α] (f : filter α) :
f =
@[protected]
theorem filter.disjoint_iff {α : Type u} {f g : filter α} :
g (s : set α) (H : s f) (t : set α) (H : t g), t
theorem filter.disjoint_of_disjoint_of_mem {α : Type u} {f g : filter α} {s t : set α} (h : t) (hs : s f) (ht : t g) :
g
theorem filter.ne_bot.not_disjoint {α : Type u} {f : filter α} {s t : set α} (hf : f.ne_bot) (hs : s f) (ht : t f) :
¬ t
theorem filter.inf_eq_bot_iff {α : Type u} {f g : filter α} :
f g = (U : set α) (H : U f) (V : set α) (H : V g), U V =
theorem pairwise.exists_mem_filter_of_disjoint {α : Type u} {ι : Type u_1} [finite ι] {l : ι } (hd : pairwise (disjoint on l)) :
(s : ι set α), ( (i : ι), s i l i) pairwise (disjoint on s)
theorem set.pairwise_disjoint.exists_mem_filter {α : Type u} {ι : Type u_1} {l : ι } {t : set ι} (hd : t.pairwise_disjoint l) (ht : t.finite) :
(s : ι set α), ( (i : ι), s i l i)
@[protected, instance]
def filter.unique {α : Type u} [is_empty α] :

There is exactly one filter on an empty type.

Equations
theorem filter.eq_top_of_ne_bot {α : Type u} [subsingleton α] (l : filter α) [l.ne_bot] :
l =

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

theorem filter.forall_mem_nonempty_iff_ne_bot {α : Type u} {f : filter α} :
( (s : set α), s f s.nonempty) f.ne_bot
@[protected, instance]
def filter.nontrivial {α : Type u} [nonempty α] :
theorem filter.eq_Inf_of_mem_iff_exists_mem {α : Type u} {S : set (filter α)} {l : filter α} (h : {s : set α}, s l (f : filter α) (H : f S), s f) :
l =
theorem filter.eq_infi_of_mem_iff_exists_mem {α : Type u} {ι : Sort x} {f : ι } {l : filter α} (h : {s : set α}, s l (i : ι), s f i) :
l = infi f
theorem filter.eq_binfi_of_mem_iff_exists_mem {α : Type u} {ι : Sort x} {f : ι } {p : ι Prop} {l : filter α} (h : {s : set α}, s l (i : ι) (_x : p i), s f i) :
l = (i : ι) (_x : p i), f i
theorem filter.infi_sets_eq {α : Type u} {ι : Sort x} {f : ι } (h : f) [ne : nonempty ι] :
(infi f).sets = (i : ι), (f i).sets
theorem filter.mem_infi_of_directed {α : Type u} {ι : Sort x} {f : ι } (h : f) [nonempty ι] (s : set α) :
s infi f (i : ι), s f i
theorem filter.mem_binfi_of_directed {α : Type u} {β : Type v} {f : β } {s : set β} (h : directed_on (f ⁻¹'o ge) s) (ne : s.nonempty) {t : set α} :
(t (i : β) (H : i s), f i) (i : β) (H : i s), t f i
theorem filter.binfi_sets_eq {α : Type u} {β : Type v} {f : β } {s : set β} (h : directed_on (f ⁻¹'o ge) s) (ne : s.nonempty) :
( (i : β) (H : i s), f i).sets = (i : β) (H : i s), (f i).sets
theorem filter.infi_sets_eq_finite {α : Type u} {ι : Type u_1} (f : ι ) :
( (i : ι), f i).sets = (t : finset ι), ( (i : ι) (H : i t), f i).sets
theorem filter.infi_sets_eq_finite' {α : Type u} {ι : Sort x} (f : ι ) :
( (i : ι), f i).sets = (t : finset (plift ι)), ( (i : plift ι) (H : i t), f i.down).sets
theorem filter.mem_infi_finite {α : Type u} {ι : Type u_1} {f : ι } (s : set α) :
s infi f (t : finset ι), s (i : ι) (H : i t), f i
theorem filter.mem_infi_finite' {α : Type u} {ι : Sort x} {f : ι } (s : set α) :
s infi f (t : finset (plift ι)), s (i : plift ι) (H : i t), f i.down
@[simp]
theorem filter.sup_join {α : Type u} {f₁ f₂ : filter (filter α)} :
f₁.join f₂.join = (f₁ f₂).join
@[simp]
theorem filter.supr_join {α : Type u} {ι : Sort w} {f : ι filter (filter α)} :
( (x : ι), (f x).join) = ( (x : ι), f x).join
@[protected, instance]
def filter.distrib_lattice {α : Type u} :
Equations
@[protected, instance]
def filter.order.coframe {α : Type u} :
Equations
theorem filter.mem_infi_finset {α : Type u} {β : Type v} {s : finset α} {f : α } {t : set β} :
(t (a : α) (H : a s), f a) (p : α set β), ( (a : α), a s p a f a) t = (a : α) (H : a s), p a
theorem filter.infi_ne_bot_of_directed' {α : Type u} {ι : Sort x} {f : ι } [nonempty ι] (hd : f) (hb : (i : ι), (f i).ne_bot) :

If `f : ι → filter α` is directed, `ι` is not empty, and `∀ i, f i ≠ ⊥`, then `infi f ≠ ⊥`. See also `infi_ne_bot_of_directed` for a version assuming `nonempty α` instead of `nonempty ι`.

theorem filter.infi_ne_bot_of_directed {α : Type u} {ι : Sort x} {f : ι } [hn : nonempty α] (hd : f) (hb : (i : ι), (f i).ne_bot) :

If `f : ι → filter α` is directed, `α` is not empty, and `∀ i, f i ≠ ⊥`, then `infi f ≠ ⊥`. See also `infi_ne_bot_of_directed'` for a version assuming `nonempty ι` instead of `nonempty α`.

theorem filter.Inf_ne_bot_of_directed' {α : Type u} {s : set (filter α)} (hne : s.nonempty) (hd : s) (hbot : s) :
theorem filter.Inf_ne_bot_of_directed {α : Type u} [nonempty α] {s : set (filter α)} (hd : s) (hbot : s) :
theorem filter.infi_ne_bot_iff_of_directed' {α : Type u} {ι : Sort x} {f : ι } [nonempty ι] (hd : f) :
(infi f).ne_bot (i : ι), (f i).ne_bot
theorem filter.infi_ne_bot_iff_of_directed {α : Type u} {ι : Sort x} {f : ι } [nonempty α] (hd : f) :
(infi f).ne_bot (i : ι), (f i).ne_bot
theorem filter.infi_sets_induct {α : Type u} {ι : Sort x} {f : ι } {s : set α} (hs : s infi f) {p : set α Prop} (uni : p set.univ) (ins : {i : ι} {s₁ s₂ : set α}, s₁ f i p s₂ p (s₁ s₂)) :
p s

#### `principal` equations #

@[simp]
theorem filter.inf_principal {α : Type u} {s t : set α} :
@[simp]
theorem filter.sup_principal {α : Type u} {s t : set α} :
@[simp]
theorem filter.supr_principal {α : Type u} {ι : Sort w} {s : ι set α} :
( (x : ι), filter.principal (s x)) = filter.principal ( (i : ι), s i)
@[simp]
theorem filter.principal_eq_bot_iff {α : Type u} {s : set α} :
s =
@[simp]
theorem filter.principal_ne_bot_iff {α : Type u} {s : set α} :
theorem set.nonempty.principal_ne_bot {α : Type u} {s : set α} :

Alias of the reverse direction of `filter.principal_ne_bot_iff`.

theorem filter.is_compl_principal {α : Type u} (s : set α) :
theorem filter.mem_inf_principal' {α : Type u} {f : filter α} {s t : set α} :
s t s f
theorem filter.mem_inf_principal {α : Type u} {f : filter α} {s t : set α} :
s {x : α | x t x s} f
theorem filter.supr_inf_principal {α : Type u} {ι : Sort x} (f : ι ) (s : set α) :
( (i : ι), f i = ( (i : ι), f i)
theorem filter.inf_principal_eq_bot {α : Type u} {f : filter α} {s : set α} :
theorem filter.mem_of_eq_bot {α : Type u} {f : filter α} {s : set α} (h : = ) :
s f
theorem filter.diff_mem_inf_principal_compl {α : Type u} {f : filter α} {s : set α} (hs : s f) (t : set α) :
s \ t
theorem filter.principal_le_iff {α : Type u} {s : set α} {f : filter α} :
(V : set α), V f s V
@[simp]
theorem filter.infi_principal_finset {α : Type u} {ι : Type w} (s : finset ι) (f : ι set α) :
( (i : ι) (H : i s), filter.principal (f i)) = filter.principal ( (i : ι) (H : i s), f i)
@[simp]
theorem filter.infi_principal {α : Type u} {ι : Type w} [finite ι] (f : ι set α) :
( (i : ι), filter.principal (f i)) = filter.principal ( (i : ι), f i)
theorem filter.infi_principal_finite {α : Type u} {ι : Type w} {s : set ι} (hs : s.finite) (f : ι set α) :
( (i : ι) (H : i s), filter.principal (f i)) = filter.principal ( (i : ι) (H : i s), f i)
theorem filter.join_mono {α : Type u} {f₁ f₂ : filter (filter α)} (h : f₁ f₂) :
f₁.join f₂.join

### Eventually #

@[protected]
def filter.eventually {α : Type u} (p : α Prop) (f : filter α) :
Prop

`f.eventually p` or `∀ᶠ x in f, p x` mean that `{x | p x} ∈ f`. E.g., `∀ᶠ x in at_top, p x` means that `p` holds true for sufficiently large `x`.

Equations
• = ({x : α | p x} f)
Instances for `filter.eventually`
theorem filter.eventually_iff {α : Type u} {f : filter α} {P : α Prop} :
(∀ᶠ (x : α) in f, P x) {x : α | P x} f
@[simp]
theorem filter.eventually_mem_set {α : Type u} {s : set α} {l : filter α} :
(∀ᶠ (x : α) in l, x s) s l
@[protected]
theorem filter.ext' {α : Type u} {f₁ f₂ : filter α} (h : (p : α Prop), (∀ᶠ (x : α) in f₁, p x) ∀ᶠ (x : α) in f₂, p x) :
f₁ = f₂
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
theorem filter.eventually_of_mem {α : Type u} {f : filter α} {P : α Prop} {U : set α} (hU : U f) (h : (x : α), x U P x) :
∀ᶠ (x : α) in f, P x
@[protected]
theorem filter.eventually.and {α : Type u} {p q : α Prop} {f : filter α} :
(∀ᶠ (x : α) in f, p x q x)
@[simp]
theorem filter.eventually_true {α : Type u} (f : filter α) :
∀ᶠ (x : α) in f, true
theorem filter.eventually_of_forall {α : Type u} {p : α Prop} {f : filter α} (hp : (x : α), p x) :
∀ᶠ (x : α) in f, p x
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
@[simp]
theorem filter.eventually_false_iff_eq_bot {α : Type u} {f : filter α} :
(∀ᶠ (x : α) in f, false) f =
@[simp]
theorem filter.eventually_const {α : Type u} {f : filter α} [t : f.ne_bot] {p : Prop} :
(∀ᶠ (x : α) in f, p) p
theorem filter.eventually_iff_exists_mem {α : Type u} {p : α Prop} {f : filter α} :
(∀ᶠ (x : α) in f, p x) (v : set α) (H : v f), (y : α), y v p y
theorem filter.eventually.exists_mem {α : Type u} {p : α Prop} {f : filter α} (hp : ∀ᶠ (x : α) in f, p x) :
(v : set α) (H : v f), (y : α), y v p y
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
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
@[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
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
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
@[simp]
theorem filter.eventually_all {α : Type u} {ι : Type u_1} [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_1} {I : set ι} (hI : I.finite) {l : filter α} {p : ι α Prop} :
(∀ᶠ (x : α) in l, (i : ι), i I p i x) (i : ι), i I (∀ᶠ (x : α) in l, p i x)
@[protected]
theorem set.finite.eventually_all {α : Type u} {ι : Type u_1} {I : set ι} (hI : I.finite) {l : filter α} {p : ι α Prop} :
(∀ᶠ (x : α) in l, (i : ι), i I p i x) (i : ι), i I (∀ᶠ (x : α) in l, p i x)

Alias of `filter.eventually_all_finite`.

@[simp]
theorem filter.eventually_all_finset {α : Type u} {ι : Type u_1} (I : finset ι) {l : filter α} {p : ι α Prop} :
(∀ᶠ (x : α) in l, (i : ι), i I p i x) (i : ι), i I (∀ᶠ (x : α) in l, p i x)
@[protected]
theorem finset.eventually_all {α : Type u} {ι : Type u_1} (I : finset ι) {l : filter α} {p : ι α Prop} :
(∀ᶠ (x : α) in l, (i : ι), i I p i x) (i : ι), i I (∀ᶠ (x : α) in l, p i x)

Alias of `filter.eventually_all_finset`.

@[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
@[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
@[simp]
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)
@[simp]
theorem filter.eventually_bot {α : Type u} {p : α Prop} :
∀ᶠ (x : α) in , p x
@[simp]
theorem filter.eventually_top {α : Type u} {p : α Prop} :
(∀ᶠ (x : α) in , p x) (x : α), p x
@[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
@[simp]
theorem filter.eventually_Sup {α : Type u} {p : α Prop} {fs : set (filter α)} :
(∀ᶠ (x : α) in , p x) (f : filter α), f fs (∀ᶠ (x : α) in f, p x)
@[simp]
theorem filter.eventually_supr {α : Type u} {ι : Sort x} {p : α Prop} {fs : ι } :
(∀ᶠ (x : α) in (b : ι), fs b, p x) (b : ι), ∀ᶠ (x : α) in fs b, p x
@[simp]
theorem filter.eventually_principal {α : Type u} {a : set α} {p : α Prop} :
(∀ᶠ (x : α) in , p x) (x : α), x a p x
theorem filter.eventually_inf {α : Type u} {f g : filter α} {p : α Prop} :
(∀ᶠ (x : α) in f g, p x) (s : set α) (H : s f) (t : set α) (H : t g), (x : α), x s t p x
theorem filter.eventually_inf_principal {α : Type u} {f : filter α} {p : α Prop} {s : set α} :
(∀ᶠ (x : α) in , p x) ∀ᶠ (x : α) in f, x s p x

### Frequently #

@[protected]
def filter.frequently {α : Type u} (p : α Prop) (f : filter α) :
Prop

`f.frequently p` or `∃ᶠ x in f, p x` mean that `{x | ¬p x} ∉ f`. E.g., `∃ᶠ x in at_top, p x` means that there exist arbitrarily large `x` for which `p` holds true.

Equations
theorem filter.eventually.frequently {α : Type u} {f : filter α} [f.ne_bot] {p : α Prop} (h : ∀ᶠ (x : α) in f, p x) :
∃ᶠ (x : α) in f, p x
theorem filter.frequently_of_forall {α : Type u} {f : filter α} [f.ne_bot] {p : α Prop} (h : (x : α), p x) :
∃ᶠ (x : α) in f, p x
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
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
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
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
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
theorem filter.frequently.exists {α : Type u} {p : α Prop} {f : filter α} (hp : ∃ᶠ (x : α) in f, p x) :
(x : α), p x
theorem filter.eventually.exists {α : Type u} {p : α Prop} {f : filter α} [f.ne_bot] (hp : ∀ᶠ (x : α) in f, p x) :
(x : α), p x
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)
theorem filter.frequently_iff {α : Type u} {f : filter α} {P : α Prop} :
(∃ᶠ (x : α) in f, P x) {U : set α}, U f ( (x : α) (H : x U), P x)
@[simp]
theorem filter.not_eventually {α : Type u} {p : α Prop} {f : filter α} :
(¬∀ᶠ (x : α) in f, p x) ∃ᶠ (x : α) in f, ¬p x
@[simp]
theorem filter.not_frequently {α : Type u} {p : α Prop} {f : filter α} :
(¬∃ᶠ (x : α) in f, p x) ∀ᶠ (x : α) in f, ¬p x
@[simp]
theorem filter.frequently_true_iff_ne_bot {α : Type u} (f : filter α) :
(∃ᶠ (x : α) in f, true) f.ne_bot
@[simp]
theorem filter.frequently_false {α : Type u} (f : filter α) :
¬∃ᶠ (x : α) in f, false
@[simp]
theorem filter.frequently_const {α : Type u} {f : filter α} [f.ne_bot] {p : Prop} :
(∃ᶠ (x : α) in f, p) p
@[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
theorem filter.frequently_or_distrib_left {α : Type u} {f : filter α} [f.ne_bot] {p : Prop} {q : α Prop} :
(∃ᶠ (x : α) in f, p q x) p ∃ᶠ (x : α) in f, q x
theorem filter.frequently_or_distrib_right {α : Type u} {f : filter α} [f.ne_bot] {p : α Prop} {q : Prop} :
(∃ᶠ (x : α) in f, p x q) (∃ᶠ (x : α) in f, p x) q
@[simp]
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)
theorem filter.frequently_imp_distrib_left {α : Type u} {f : filter α} [f.ne_bot] {p : Prop} {q : α Prop} :
(∃ᶠ (x : α) in f, p q x) p (∃ᶠ (x : α) in f, q x)
theorem filter.frequently_imp_distrib_right {α : Type u} {f : filter α} [f.ne_bot] {p : α Prop} {q : Prop} :
(∃ᶠ (x : α) in f, p x q) (∀ᶠ (x : α) in f, p x) q
@[simp]
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
@[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
@[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
@[simp]
theorem filter.frequently_bot {α : Type u} {p : α Prop} :
¬∃ᶠ (x : α) in , p x
@[simp]
theorem filter.frequently_top {α : Type u} {p : α Prop} :
(∃ᶠ (x : α) in , p x) (x : α), p x
@[simp]
theorem filter.frequently_principal {α : Type u} {a : set α} {p : α Prop} :
(∃ᶠ (x : α) in , p x) (x : α) (H : x a), p x
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
@[simp]
theorem filter.frequently_Sup {α : Type u} {p : α Prop} {fs : set (filter α)} :
(∃ᶠ (x : α) in , p x) (f : filter α) (H : f fs), ∃ᶠ (x : α) in f, p x
@[simp]
theorem filter.frequently_supr {α : Type u} {β : Type v} {p : α Prop} {fs : β } :
(∃ᶠ (x : α) in (b : β), fs b, p x) (b : β), ∃ᶠ (x : α) in fs b, p x
theorem filter.eventually.choice {α : Type u} {β : Type v} {r : α β Prop} {l : filter α} [l.ne_bot] (h : ∀ᶠ (x : α) in l, (y : β), r x y) :
(f : α β), ∀ᶠ (x : α) in l, r x (f x)

### Relation “eventually equal” #

def filter.eventually_eq {α : Type u} {β : Type v} (l : filter α) (f g : α β) :
Prop

Two functions `f` and `g` are eventually equal along a filter `l` if the set of `x` such that `f x = g x` belongs to `l`.

Equations
theorem filter.eventually_eq.eventually {α : Type u} {β : Type v} {l : filter α} {f g : α β} (h : f =ᶠ[l] g) :
∀ᶠ (x : α) in l, f x = g x
theorem filter.eventually_eq.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)
theorem filter.eventually_eq_set {α : Type u} {s t : set α} {l : filter α} :
s =ᶠ[l] t ∀ᶠ (x : α) in l, x s x t
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.eventually_eq_set`.

theorem filter.eventually_eq.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.eventually_eq_set`.

@[simp]
theorem filter.eventually_eq_univ {α : Type u} {s : set α} {l : filter α} :
s l
theorem filter.eventually_eq.exists_mem {α : Type u} {β : Type v} {l : filter α} {f g : α β} (h : f =ᶠ[l] g) :
(s : set α) (H : s l), g s
theorem filter.eventually_eq_of_mem {α : Type u} {β : Type v} {l : filter α} {f g : α β} {s : set α} (hs : s l) (h : g s) :
f =ᶠ[l] g
theorem filter.eventually_eq_iff_exists_mem {α : Type u} {β : Type v} {l : filter α} {f g : α β} :
f =ᶠ[l] g (s : set α) (H : s l), g s
theorem filter.eventually_eq.filter_mono {α : Type u} {β : Type v} {l l' : filter α} {f g : α β} (h₁ : f =ᶠ[l] g) (h₂ : l' l) :
f =ᶠ[l'] g
@[refl]
theorem filter.eventually_eq.refl {α : Type u} {β : Type v} (l : filter α) (f : α β) :
f =ᶠ[l] f
theorem filter.eventually_eq.rfl {α : Type u} {β : Type v} {l : filter α} {f : α β} :
f =ᶠ[l] f
@[symm]
theorem filter.eventually_eq.symm {α : Type u} {β : Type v} {f g : α β} {l : filter α} (H : f =ᶠ[l] g) :
g =ᶠ[l] f
@[trans]
theorem filter.eventually_eq.trans {α : Type u} {β : Type v} {l : filter α} {f g h : α β} (H₁ : f =ᶠ[l] g) (H₂ : g =ᶠ[l] h) :
f =ᶠ[l] h
theorem filter.eventually_eq.prod_mk {α : Type u} {β : Type v} {γ : Type w} {l : filter α} {f f' : α β} (hf : f =ᶠ[l] f') {g g' : α γ} (hg : g =ᶠ[l] g') :
(λ (x : α), (f x, g x)) =ᶠ[l] λ (x : α), (f' x, g' x)
theorem filter.eventually_eq.fun_comp {α : Type u} {β : Type v} {γ : Type w} {f g : α β} {l : filter α} (H : f =ᶠ[l] g) (h : β γ) :
h f =ᶠ[l] h g
theorem filter.eventually_eq.comp₂ {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} {f f' : α β} {g g' : α γ} {l : filter α} (Hf : f =ᶠ[l] f') (h : β γ δ) (Hg : g =ᶠ[l] g') :
(λ (x : α), h (f x) (g x)) =ᶠ[l] λ (x : α), h (f' x) (g' x)
theorem filter.eventually_eq.add {α : Type u} {β : Type v} [has_add β] {f f' g g' : α β} {l : filter α} (h : f =ᶠ[l] g) (h' : f' =ᶠ[l] g') :
(λ (x : α), f x + f' x) =ᶠ[l] λ (x : α), g x + g' x
theorem filter.eventually_eq.mul {α : Type u} {β : Type v} [has_mul β] {f f' g g' : α β} {l : filter α} (h : f =ᶠ[l] g) (h' : f' =ᶠ[l] g') :
(λ (x : α), f x * f' x) =ᶠ[l] λ (x : α), g x * g' x
theorem filter.eventually_eq.neg {α : Type u} {β : Type v} [has_neg β] {f g : α β} {l : filter α} (h : f =ᶠ[l] g) :
(λ (x : α), -f x) =ᶠ[l] λ (x : α), -g x
theorem filter.eventually_eq.inv {α : Type u} {β : Type v} [has_inv β] {f g : α β} {l : filter α} (h : f =ᶠ[l] g) :
(λ (x : α), (f x)⁻¹) =ᶠ[l] λ (x : α), (g x)⁻¹
theorem filter.eventually_eq.sub {α : Type u} {β : Type v} [has_sub β] {f f' g g' : α β} {l : filter α} (h : f =ᶠ[l] g) (h' : f' =ᶠ[l] g') :
(λ (x : α), f x - f' x) =ᶠ[l] λ (x : α), g x - g' x
theorem filter.eventually_eq.div {α : Type u} {β : Type v} [has_div β] {f f' g g' : α β} {l : filter α} (h : f =ᶠ[l] g) (h' : f' =ᶠ[l] g') :
(λ (x : α), f x / f' x) =ᶠ[l] λ (x : α), g x / g' x
theorem filter.eventually_eq.const_vadd {α : Type u} {β : Type v} {𝕜 : Type u_1} [ β] {l : filter α} {f g : α β} (h : f =ᶠ[l] g) (c : 𝕜) :
(λ (x : α), c +ᵥ f x) =ᶠ[l] λ (x : α), c +ᵥ g x
theorem filter.eventually_eq.const_smul {α : Type u} {β : Type v} {𝕜 : Type u_1} [ β] {l : filter α} {f g : α β} (h : f =ᶠ[l] g) (c : 𝕜) :
(λ (x : α), c f x) =ᶠ[l] λ (x : α), c g x
theorem filter.eventually_eq.vadd {α : Type u} {β : Type v} {𝕜 : Type u_1} [ β] {l : filter α} {f f' : α 𝕜} {g g' : α β} (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') :
(λ (x : α), f x +ᵥ g x) =ᶠ[l] λ (x : α), f' x +ᵥ g' x
theorem filter.eventually_eq.smul {α : Type u} {β : Type v} {𝕜 : Type u_1} [ β] {l : filter α} {f f' : α 𝕜} {g g' : α β} (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') :
(λ (x : α), f x g x) =ᶠ[l] λ (x : α), f' x g' x
theorem filter.eventually_eq.sup {α : Type u} {β : Type v} [has_sup β] {l : filter α} {f f' g g' : α β} (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') :
(λ (x : α), f x g x) =ᶠ[l] λ (x : α), f' x g' x
theorem filter.eventually_eq.inf {α : Type u} {β : Type v} [has_inf β] {l : filter α} {f f' g g' : α β} (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') :
(λ (x : α), f x g x) =ᶠ[l] λ (x : α), f' x g' x
theorem filter.eventually_eq.preimage {α : Type u} {β : Type v} {l : filter α} {f g : α β} (h : f =ᶠ[l] g) (s : set β) :
theorem filter.eventually_eq.inter {α : Type u} {s t s' t' : set α} {l : filter α} (h : s =ᶠ[l] t) (h' : s' =ᶠ[l] t') :
s s' =ᶠ[l] t t'
theorem filter.eventually_eq.union {α : Type u} {s t s' t' : set α} {l : filter α} (h : s =ᶠ[l] t) (h' : s' =ᶠ[l] t') :
s s' =ᶠ[l] t t'
theorem filter.eventually_eq.compl {α : Type u} {s t : set α} {l : filter α} (h : s =ᶠ[l] t) :
theorem filter.eventually_eq.diff {α : Type u} {s t s' t' : set α} {l : filter α} (h : s =ᶠ[l] t) (h' : s' =ᶠ[l] t') :
s \ s' =ᶠ[l] t \ t'
theorem filter.eventually_eq_empty {α : Type u} {s : set α} {l : filter α} :
s =ᶠ[l] ∀ᶠ (x : α) in l, x s
theorem filter.inter_eventually_eq_left {α : Type u} {s t : set α} {l : filter α} :
s t =ᶠ[l] s ∀ᶠ (x : α) in l, x s x t
theorem filter.inter_eventually_eq_right {α : Type u} {s t : set α} {l : filter α} :
s t =ᶠ[l] t ∀ᶠ (x : α) in l, x t x s
@[simp]
theorem filter.eventually_eq_principal {α : Type u} {β : Type v} {s : set α} {f g : α β} :
g s
theorem filter.eventually_eq_inf_principal_iff {α : Type u} {β : Type v} {F : filter α} {s : set α} {f g : α β} :
f =ᶠ[] g ∀ᶠ (x : α) in F, x s f x = g x
theorem filter.eventually_eq.sub_eq {α : Type u} {β : Type v} [add_group β] {f g : α β} {l : filter α} (h : f =ᶠ[l] g) :
f - g =ᶠ[l] 0
theorem filter.eventually_eq_iff_sub {α : Type u} {β : Type v} [add_group β] {f g : α β} {l : filter α} :
f =ᶠ[l] g f - g =ᶠ[l] 0
def filter.eventually_le {α : Type u} {β : Type v} [has_le β] (l : filter α) (f g : α β) :
Prop

A function `f` is eventually less than or equal to a function `g` at a filter `l`.

Equations
theorem filter.eventually_le.congr {α : Type u} {β : Type v} [has_le β] {l : filter α} {f f' g g' : α β} (H : f ≤ᶠ[l] g) (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') :
f' ≤ᶠ[l] g'
theorem filter.eventually_le_congr {α : Type u} {β : Type v} [has_le β] {l : filter α} {f f' g g' : α β} (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') :
f ≤ᶠ[l] g f' ≤ᶠ[l] g'
theorem filter.eventually_eq.le {α : Type u} {β : Type v} [preorder β] {l : filter α} {f g : α β} (h : f =ᶠ[l] g) :
@[refl]
theorem filter.eventually_le.refl {α : Type u} {β : Type v} [preorder β] (l : filter α) (f : α β) :
theorem filter.eventually_le.rfl {α : Type u} {β : Type v} [preorder β] {l : filter α} {f : α β} :
@[trans]
theorem filter.eventually_le.trans {α : Type u} {β : Type v} [preorder β] {l : filter α} {f g h : α β} (H₁ : f ≤ᶠ[l] g) (H₂ : g ≤ᶠ[l] h) :
@[trans]
theorem filter.eventually_eq.trans_le {α : Type u} {β : Type v} [preorder β] {l : filter α} {f g h : α β} (H₁ : f =ᶠ[l] g) (H₂ : g ≤ᶠ[l] h) :
@[trans]
theorem filter.eventually_le.trans_eq {α : Type u} {β : Type v} [preorder β] {l : filter α} {f g h : α β} (H₁ : f ≤ᶠ[l] g) (H₂ : g =ᶠ[l] h) :
theorem filter.eventually_le.antisymm {α : Type u} {β : Type v} {l : filter α} {f g : α β} (h₁ : f ≤ᶠ[l] g) (h₂ : g ≤ᶠ[l] f) :
f =ᶠ[l] g
theorem filter.eventually_le_antisymm_iff {α : Type u} {β : Type v} {l : filter α} {f g : α β} :
f =ᶠ[l] g f ≤ᶠ[l] g g ≤ᶠ[l] f
theorem filter.eventually_le.le_iff_eq {α : Type u} {β : Type v} {l : filter α} {f g : α β} (h : f ≤ᶠ[l] g) :
g ≤ᶠ[l] f g =ᶠ[l] f
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
theorem filter.eventually.ne_top_of_lt {α : Type u} {β : Type v} [order_top β] {l : filter α} {f g : α β} (h : ∀ᶠ (x : α) in l, f x < g x) :
∀ᶠ (x : α) in l, f x
theorem filter.eventually.lt_top_of_ne {α : Type u} {β : Type v} [order_top β] {l : filter α} {f : α β} (h : ∀ᶠ (x : α) in l, f x ) :
∀ᶠ (x : α) in l, f x <
theorem filter.eventually.lt_top_iff_ne_top {α : Type u} {β : Type v} [order_top β] {l : filter α} {f : α β} :
(∀ᶠ (x : α) in l, f x < ) ∀ᶠ (x : α) in l, f x
theorem filter.eventually_le.inter {α : Type u} {s t s' t' : set α} {l : filter α} (h : s ≤ᶠ[l] t) (h' : s' ≤ᶠ[l] t') :
s s' ≤ᶠ[l] t t'
theorem filter.eventually_le.union {α : Type u} {s t s' t' : set α} {l : filter α} (h : s ≤ᶠ[l] t) (h' : s' ≤ᶠ[l] t') :
s s' ≤ᶠ[l] t t'
theorem filter.eventually_le.compl {α : Type u} {s t : set α} {l : filter α} (h : s ≤ᶠ[l] t) :
theorem filter.eventually_le.diff {α : Type u} {s t s' t' : set α} {l : filter α} (h : s ≤ᶠ[l] t) (h' : t' ≤ᶠ[l] s') :
s \ s' ≤ᶠ[l] t \ t'
theorem filter.set_eventually_le_iff_mem_inf_principal {α : Type u} {s t : set α} {l : filter α} :
s ≤ᶠ[l] t t
theorem filter.set_eventually_le_iff_inf_principal_le {α : Type u} {s t : set α} {l : filter α} :
theorem filter.set_eventually_eq_iff_inf_principal {α : Type u} {s t : set α} {l : filter α} :
s =ᶠ[l] t =
theorem filter.eventually_le.mul_le_mul {α : Type u} {β : Type v} [pos_mul_mono β] [mul_pos_mono β] {l : filter α} {f₁ f₂ g₁ g₂ : α β} (hf : f₁ ≤ᶠ[l] f₂) (hg : g₁ ≤ᶠ[l] g₂) (hg₀ : 0 ≤ᶠ[l] g₁) (hf₀ : 0 ≤ᶠ[l] f₂) :
f₁ * g₁ ≤ᶠ[l] f₂ * g₂
theorem eventually_le.add_le_add {α : Type u} {β : Type v} [has_add β] [preorder β] {l : filter α} {f₁ f₂ g₁ g₂ : α β} (hf : f₁ ≤ᶠ[l] f₂) (hg : g₁ ≤ᶠ[l] g₂) :
f₁ + g₁ ≤ᶠ[l] f₂ + g₂
theorem filter.eventually_le.mul_le_mul' {α : Type u} {β : Type v} [has_mul β] [preorder β] {l : filter α} {f₁ f₂ g₁ g₂ : α β} (hf : f₁ ≤ᶠ[l] f₂) (hg : g₁ ≤ᶠ[l] g₂) :
f₁ * g₁ ≤ᶠ[l] f₂ * g₂
theorem filter.eventually_le.mul_nonneg {α : Type u} {β : Type v} {l : filter α} {f g : α β} (hf : 0 ≤ᶠ[l] f) (hg : 0 ≤ᶠ[l] g) :
0 ≤ᶠ[l] f * g
theorem filter.eventually_sub_nonneg {α : Type u} {β : Type v} [ordered_ring β] {l : filter α} {f g : α β} :
0 ≤ᶠ[l] g - f f ≤ᶠ[l] g
theorem filter.eventually_le.sup {α : Type u} {β : Type v} {l : filter α} {f₁ f₂ g₁ g₂ : α β} (hf : f₁ ≤ᶠ[l] f₂) (hg : g₁ ≤ᶠ[l] g₂) :
f₁ g₁ ≤ᶠ[l] f₂ g₂
theorem filter.eventually_le.sup_le {α : Type u} {β : Type v} {l : filter α} {f g h : α β} (hf : f ≤ᶠ[l] h) (hg : g ≤ᶠ[l] h) :
f g ≤ᶠ[l] h
theorem filter.eventually_le.le_sup_of_le_left {α : Type u} {β : Type v} {l : filter α} {f g h : α β} (hf : h ≤ᶠ[l] f) :
h ≤ᶠ[l] f g
theorem filter.eventually_le.le_sup_of_le_right {α : Type u} {β : Type v} {l : filter α} {f g h : α β} (hg : h ≤ᶠ[l] g) :
h ≤ᶠ[l] f g
theorem filter.join_le {α : Type u} {f : filter (filter α)} {l : filter α} (h : ∀ᶠ (m : filter α) in f, m l) :
f.join l

### Push-forwards, pull-backs, and the monad structure #

def filter.map {α : Type u} {β : Type v} (m : α β) (f : filter α) :

The forward map of a filter

Equations
Instances for `filter.map`
@[simp]
theorem filter.map_principal {α : Type u} {β : Type v} {s : set α} {f : α β} :
@[simp]
theorem filter.eventually_map {α : Type u} {β : Type v} {f : filter α} {m : α β} {P : β Prop} :
(∀ᶠ (b : β) in f, P b) ∀ᶠ (a : α) in f, P (m a)
@[simp]
theorem filter.frequently_map {α : Type u} {β : Type v} {f : filter α} {m : α β} {P : β Prop} :
(∃ᶠ (b : β) in f, P b) ∃ᶠ (a : α) in f, P (m a)
@[simp]
theorem filter.mem_map {α : Type u} {β : Type v} {f : filter α} {m : α β} {t : set β} :
t f m ⁻¹' t f
theorem filter.mem_map' {α : Type u} {β : Type v} {f : filter α} {m : α β} {t : set β} :
t f {x : α | m x t} f
theorem filter.image_mem_map {α : Type u} {β : Type v} {f : filter α} {m : α β} {s : set α} (hs : s f) :
m '' s f
theorem filter.image_mem_map_iff {α : Type u} {β : Type v} {f : filter α} {m : α β} {s : set α} (hf : function.injective m) :
m '' s f s f
theorem filter.range_mem_map {α : Type u} {β : Type v} {f : filter α} {m : α β} :
f
theorem filter.mem_map_iff_exists_image {α : Type u} {β : Type v} {f : filter α} {m : α β} {t : set β} :
t f (s : set α) (H : s f), m '' s t
@[simp]
theorem filter.map_id {α : Type u} {f : filter α} :
= f
@[simp]
theorem filter.map_id' {α : Type u} {f : filter α} :
filter.map (λ (x : α), x) f = f
@[simp]
theorem filter.map_compose {α : Type u} {β : Type v} {γ : Type w} {m : α β} {m' : β γ} :
= filter.map (m' m)
@[simp]
theorem filter.map_map {α : Type u} {β : Type v} {γ : Type w} {f : filter α} {m : α β} {m' : β γ} :
f) = filter.map (m' m) f
theorem filter.map_congr {α : Type u} {β : Type v} {m₁ m₂ : α β} {f : filter α} (h : m₁ =ᶠ[f] m₂) :
f = f

If functions `m₁` and `m₂` are eventually equal at a filter `f`, then they map this filter to the same filter.

def filter.comap {α : Type u} {β : Type v} (m : α β) (f : filter β) :

The inverse map of a filter. A set `s` belongs to `filter.comap m f` if either of the following equivalent conditions hold.

1. There exists a set `t ∈ f` such that `m ⁻¹' t ⊆ s`. This is used as a definition.
2. The set `{y | ∀ x, m x = y → x ∈ s}` belongs to `f`, see `filter.mem_comap'`.
3. The set `(m '' sᶜ)ᶜ` belongs to `f`, see `filter.mem_comap_iff_compl` and `filter.compl_mem_comap`.
Equations
Instances for `filter.comap`
theorem filter.mem_comap' {α : Type u} {β : Type v} {f : α β} {l : filter β} {s : set α} :
s l {y : β | ⦃x : α⦄, f x = y x s} l
theorem filter.mem_comap_prod_mk {α : Type u} {β : Type v} {x : α} {s : set β} {F : filter × β)} :
s F {p : α × β | p.fst = x p.snd s} F

RHS form is used, e.g., in the definition of `uniform_space`.

@[simp]
theorem filter.eventually_comap {α : Type u} {β : Type v} {f : α β} {l : filter β} {p : α Prop} :
(∀ᶠ (a : α) in l, p a) ∀ᶠ (b : β) in l, (a : α), f a = b p a
@[simp]
theorem filter.frequently_comap {α : Type u} {β : Type v} {f : α β} {l : filter β} {p : α Prop} :
(∃ᶠ (a : α) in l, p a) ∃ᶠ (b : β) in l, (a : α), f a = b p a
theorem filter.mem_comap_iff_compl {α : Type u} {β : Type v} {f : α β} {l : filter β} {s : set α} :
s l (f '' s) l
theorem filter.compl_mem_comap {α : Type u} {β : Type v} {f : α β} {l : filter β} {s : set α} :
s l (f '' s) l
def filter.bind {α : Type u} {β : Type v} (f : filter α) (m : α ) :

The monadic bind operation on filter is defined the usual way in terms of `map` and `join`.

Unfortunately, this `bind` does not result in the expected applicative. See `filter.seq` for the applicative instance.

Equations
def filter.seq {α : Type u} {β : Type v} (f : filter β)) (g : filter α) :

The applicative sequentiation operation. This is not induced by the bind operation.

Equations
@[protected, instance]

`pure x` is the set of sets that contain `x`. It is equal to `𝓟 {x}` but with this definition we have `s ∈ pure a` defeq `a ∈ s`.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem filter.pure_sets {α : Type u} (a : α) :
.sets = {s : set α | a s}
@[simp]
theorem filter.mem_pure {α : Type u} {a : α} {s : set α} :
a s
@[simp]
theorem filter.eventually_pure {α : Type u} {a : α} {p : α Prop} :
(∀ᶠ (x : α) in , p x) p a
@[simp]
theorem filter.principal_singleton {α : Type u} (a : α) :
@[simp]
theorem filter.map_pure {α : Type u} {β : Type v} (f : α β) (a : α) :
@[simp]
theorem filter.join_pure {α : Type u} (f : filter α) :
.join = f
@[simp]
theorem filter.pure_bind {α : Type u} {β : Type v} (a : α) (m : α ) :
.bind m = m a
@[protected]

Equations
@[protected]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem filter.map_def {α β : Type u_1} (m : α β) (f : filter α) :
m <\$> f = f
@[simp]
theorem filter.bind_def {α β : Type u_1} (f : filter α) (m : α ) :
f >>= m = f.bind m

#### `map` and `comap` equations #

@[simp]
theorem filter.mem_comap {α : Type u} {β : Type v} {g : filter β} {m : α β} {s : set α} :
s g (t : set β) (H : t g), m ⁻¹' t s
theorem filter.preimage_mem_comap {α : Type u} {β : Type v} {g : filter β} {m : α β} {t : set β} (ht : t g) :
m ⁻¹' t g
theorem filter.eventually.comap {α : Type u} {β : Type v} {g : filter β} {p : β Prop} (hf : ∀ᶠ (b : β) in g, p b) (f : α β) :
∀ᶠ (a : α) in g, p (f a)
theorem filter.comap_id {α : Type u} {f : filter α} :
= f
theorem filter.comap_id' {α : Type u} {f : filter α} :
filter.comap (λ (x : α), x) f = f
theorem filter.comap_const_of_not_mem {α : Type u} {β : Type v} {g : filter β} {t : set β} {x : β} (ht : t