# mathlibdocumentation

order.filter.basic

# Theory of filters on sets #

## 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 tx yy t} {h₃ : ∀ {x y : set α}, x ty tx 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.setsf = 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 sx 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 iss 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 iss 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 iss 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 sU 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 fp 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`
@[protected, instance]
def filter.inhabited {α : Type u} :
Equations
@[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 gx 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
• basic : ∀ {α : Type u} {g : set (set α)} {s : set α}, s g
• univ : ∀ {α : Type u} {g : set (set α)},
• superset : ∀ {α : Type u} {g : set (set α)} {s t : set α}, s t
• inter : ∀ {α : Type u} {g : set (set α)} {s t : set α}, (s t)

`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
@[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 sx 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 IV 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.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 =
@[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
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 sp 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.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 ip 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 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 tx 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 fs 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)
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 UP 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
@[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 vp 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 vp y
theorem filter.eventually.mp {α : Type u} {p q : α → Prop} {f : filter α} (hp : ∀ᶠ (x : α) in f, p x) (hq : ∀ᶠ (x : α) in f, p xq 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 xq 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 Ip 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 Ip 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 Ip 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 Ip 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} {β : Type v} {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 ap 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 tp x
theorem filter.eventually_inf_principal {α : Type u} {f : filter α} {p : α → Prop} {s : set α} :
(∀ᶠ (x : α) in , p x) ∀ᶠ (x : α) in f, x sp 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
• = ¬∀ᶠ (x : α) in f, ¬p x
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 xq 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 xq 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 xq 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

### 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
• f =ᶠ[l] g = ∀ᶠ (x : α) in l, f x = g x
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 sx t
theorem filter.inter_eventually_eq_right {α : Type u} {s t : set α} {l : filter α} :
s t =ᶠ[l] t ∀ᶠ (x : α) in l, x tx 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 sf 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.eventually_le.mul_le_mul {α : Type u} {β : Type v} {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 f l` if either of the following equivalent conditions hold.

1. There exists a set `t ∈ l` such that `f ⁻¹' t ⊆ s`. This is used as a definition.
2. The set `{y | ∀ x, f x = y → x ∈ s}` belongs to `l`, see `filter.mem_comap'`.
3. The set `(f '' sᶜ)ᶜ` belongs to `l`, 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 = yx s} l
@[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 = bp 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_const_of_not_mem {α : Type u} {β : Type v} {g : filter β} {t : set β} {x : β} (ht : t g) (hx : x t) :
filter.comap (λ (y : α), x) g =
theorem filter.comap_const_of_mem {α : Type u} {β : Type v} {g : filter β} {x : β} (h : ∀ (t : set β), t gx t) :
filter.comap (λ (y : α), x) g =
theorem filter.map_const {α : Type u} {β : Type v} {f : filter α} [f.ne_bot] {c : β} :
filter.map (λ (x : α), c) f =
theorem filter.comap_comap {α : Type u} {β : Type v} {γ : Type w} {f : filter α} {m : γ → β} {n : β → α} :
f) = filter.comap (n m) f

The variables in the following lemmas are used as in this diagram:

``````    φ
α → β
θ ↓   ↓ ψ
γ → δ
ρ
``````
theorem filter.map_comm {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} {φ : α → β} {θ : α → γ} {ψ : β → δ} {ρ : γ → δ} (H : ψ φ = ρ θ) (F : filter α) :
F) = F)
theorem filter.comap_comm {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} {φ : α → β} {θ : α → γ} {ψ : β → δ} {ρ : γ → δ} (H : ψ φ = ρ θ) (G : filter δ) :
G) = G)
theorem function.semiconj.filter_map {α : Type u} {β : Type v} {f : α → β} {ga : α → α} {gb : β → β} (h : gb) :
theorem commute.filter_map {α : Type u} {f g : α → α} (h : g) :
theorem function.semiconj.filter_comap {α : Type u} {β : Type v} {f : α → β} {ga : α → α} {gb : β → β} (h : gb) :
theorem commute.filter_comap {α : Type u} {f g : α → α} (h : g) :
@[simp]
theorem filter.comap_principal {α : Type u} {β : Type v} {m : α → β} {t : set β} :
@[simp]
theorem filter.comap_pure {α : Type u} {β : Type v} {m : α → β} {b : β} :
theorem filter.map_le_iff_le_comap {α : Type u} {β : Type v} {f : filter α} {g : filter β} {m : α → β} :
f g f g
theorem filter.gc_map_comap {α : Type u} {β : Type v} (m : α → β) :
theorem filter.map_mono {α : Type u} {β : Type v} {m : α → β} :
theorem filter.comap_mono {α : Type u} {β : Type v} {m : α → β} :
@[simp]
theorem filter.map_bot {α : Type u} {β : Type v} {m : α → β} :
@[simp]
theorem filter.map_sup {α : Type u} {β : Type v} {f₁ f₂ : filter α} {m : α → β} :
(f₁ f₂) = f₁ f₂
@[simp]
theorem filter.map_supr {α : Type u} {β : Type v} {ι : Sort x} {m : α → β} {f : ι → } :
(⨆ (i : ι), f i) = ⨆ (i : ι), (f i)
@[simp]
theorem filter.map_top {α : Type u} {β : Type v} (f : α → β) :
@[simp]
theorem filter.comap_top {α : Type u} {β : Type v} {m : α → β} :
@[simp]
theorem filter.comap_inf {α : Type u} {β : Type v} {g₁ g₂ : filter β} {m : α → β} :
(g₁ g₂) = g₁ g₂
@[simp]
theorem filter.comap_infi {α : Type u} {β : Type v} {ι : Sort x} {m : α → β} {f : ι → } :
(⨅ (i : ι), f i) = ⨅ (i : ι), (f i)
theorem filter.le_comap_top {α : Type u} {β : Type v} (f : α → β) (l : filter α) :
l
theorem filter.map_comap_le {α : Type u} {β : Type v} {g : filter β} {m : α → β} :
g) g
theorem filter.le_comap_map {α : Type u} {β : Type v} {f : filter α} {m : α → β} :
f f)
@[simp]
theorem filter.comap_bot {α : Type u} {β : Type v} {m : α → β} :
theorem filter.comap_inf_principal_range {α : Type u} {β : Type v} {g : filter β} {m : α → β} :
(g = g
theorem filter.disjoint_comap {α : Type u} {β : Type v} {g₁ g₂ : filter β} {m : α → β} (h : disjoint g₁ g₂) :
disjoint g₁) g₂)
theorem filter.comap_supr {α : Type u} {β : Type v} {ι : Sort u_1} {f : ι → } {m : α → β} :
(supr f) = ⨆ (i : ι), (f i)
theorem filter.comap_Sup {α : Type u} {β : Type v} {s : set (filter β)} {m : α → β} :
(has_Sup.Sup s) = ⨆ (f : filter β) (H : f s), f
theorem filter.comap_sup {α : Type u} {β : Type v} {g₁ g₂ : filter β} {m : α → β} :
(g₁ g₂) = g₁ g₂
theorem filter.map_comap {α : Type u} {β : Type v} (f : filter β) (m : α → β) :
f) =
theorem filter.map_comap_of_mem {α : Type u} {β : Type v} {f : filter β} {m : α → β} (hf : f) :
f) = f
@[protected, instance]
def filter.can_lift {α : Type u} {β : Type v} [ β] :
Equations
theorem filter.comap_le_comap_iff {α : Type u} {β : Type v} {f g : filter β} {m : α → β} (hf : f) :
f g f g
theorem filter.map_comap_of_surjective {α : Type u} {β : Type v} {f : α → β} (hf : function.surjective f) (l : filter β) :
l) = l
theorem function.surjective.filter_map_top {α : Type u} {β : Type v} {f : α → β} (hf : function.surjective f) :
theorem filter.subtype_coe_map_comap {α : Type u} (s : set α) (f : filter α) :
=
theorem filter.subtype_coe_map_comap_prod {α : Type u} (s : set α) (f : filter × α)) :
theorem filter.image_mem_of_mem_comap {α : Type u} {β : Type v} {f : filter α} {c : β → α} (h : f) {W : set β} (W_in : W f) :
c '' W f
theorem filter.image_coe_mem_of_mem_comap {α : Type u} {f : filter α} {U : set α} (h : U f) {W : set U} (W_in : W ) :
f
theorem filter.comap_map {α : Type u} {β : Type v} {f : filter α} {m : α → β} (h : function.injective m) :
f) = f
theorem filter.mem_comap_iff {α : Type u} {β : Type v} {f : filter β} {m : α → β} (inj : function.injective m) (large : f) {S : set α} :
S f m '' S f
theorem filter.map_le_map_iff_of_inj_on {α : Type u} {β : Type v} {l₁ l₂ : filter α} {f : α → β} {s : set α} (h₁ : s l₁) (h₂ : s l₂) (hinj : s) :
l₁ l₂ l₁ l₂
theorem filter.map_le_map_iff {α : Type u} {β : Type v} {f g : filter α} {m : α → β} (hm : function.injective m) :
f g f g
theorem filter.map_eq_map_iff_of_inj_on {α : Type u} {β : Type v} {f g : filter α} {m : α → β} {s : set α} (hsf : s f) (hsg : s g) (hm : s) :
f = g f = g
theorem filter.map_inj {α : Type u} {β : Type v} {f g : filter α} {m : α → β} (hm : function.injective m) :
f = g f = g
theorem filter.map_injective {α : Type u} {β : Type v} {m : α → β} (hm : function.injective m) :
theorem filter.comap_ne_bot_iff {α : Type u} {β : Type v} {f : filter β} {m : α → β} :
f).ne_bot ∀ (t : set β), t f(∃ (a : α), m a t)
theorem filter.comap_ne_bot {α : Type u} {β : Type v} {f : filter β} {m : α → β} (hm : ∀ (t : set β), t f(∃ (a : α), m a t)) :
f).ne_bot
theorem filter.comap_ne_bot_iff_frequently {α : Type u} {β : Type v} {f : filter β} {m : α → β} :
f).ne_bot ∃ᶠ (y : β) in f, y
theorem filter.comap_ne_bot_iff_compl_range {α : Type u} {β : Type v} {f : filter β} {m : α → β} :
theorem filter.ne_bot.comap_of_range_mem {α : Type u} {β : Type v} {f : filter β} {m : α → β} (hf : f.ne_bot) (hm : f) :
f).ne_bot
@[simp]
theorem filter.comap_fst_ne_bot_iff {α : Type u} {β : Type v} {f : filter α} :
@[instance]
theorem filter.comap_fst_ne_bot {α : Type u} {β : Type v} [nonempty β] {f : filter α} [f.ne_bot] :
@[simp]
theorem filter.comap_snd_ne_bot_iff {α : Type u} {β : Type v} {f : filter β} :
@[instance]
theorem filter.comap_snd_ne_bot {α : Type u} {β : Type v} [nonempty α] {f : filter β} [f.ne_bot] :
theorem filter.comap_eval_ne_bot_iff' {ι : Type u_1} {α : ι → Type u_2} {i : ι} {f : filter (α i)} :
f).ne_bot (∀ (j : ι), nonempty (α j)) f.ne_bot
@[simp]
theorem filter.comap_eval_ne_bot_iff {ι : Type u_1} {α : ι → Type u_2} [∀ (j : ι), nonempty (α j)] {i : ι} {f : filter (α i)} :
@[instance]
theorem filter.comap_eval_ne_bot {ι : Type u_1} {α : ι → Type u_2} [∀ (j : ι), nonempty (α j)] (i : ι) (f : filter (α i)) [f.ne_bot] :
f).ne_bot
theorem filter.comap_inf_principal_ne_bot_of_image_mem {α : Type u} {β : Type v} {f : filter β} {m : α → β} (hf : f.ne_bot) {s : set α} (hs : m '' s f) :
theorem filter.comap_coe_ne_bot_of_le_principal {γ : Type w} {s : set γ} {l : filter γ} [h : l.ne_bot] (h' : l ) :
l).ne_bot
theorem filter.ne_bot.comap_of_surj {α : Type u} {β : Type v} {f : filter β} {m : α → β} (hf : f.ne_bot) (hm : function.surjective m) :
f).ne_bot
theorem filter.ne_bot.comap_of_image_mem {α : Type u} {β : Type v} {f : filter β} {m : α → β} (hf : f.ne_bot) {s : set α} (hs : m '' s f) :
f).ne_bot
@[simp]
theorem filter.map_eq_bot_iff {α : Type u} {β : Type v} {f : filter α} {m : α → β} :
f = f =
theorem filter.map_ne_bot_iff {α : Type u} {β : Type v} (f : α → β) {F : filter α} :
theorem filter.ne_bot.map {α : Type u} {β : Type v} {f : filter α} (hf : f.ne_bot) (m : α → β) :
f).ne_bot
theorem filter.ne_bot.of_map {α : Type u} {β : Type v} {f : filter α} {m : α → β} :
f).ne_bot → f.ne_bot
@[protected, instance]
def filter.map_ne_bot {α : Type u} {β : Type v} {f : filter α} {m : α → β} [hf : f.ne_bot] :
f).ne_bot
theorem filter.sInter_comap_sets {α : Type u} {β : Type v} (f : α → β) (F : filter β) :
⋂₀ F).sets = ⋂ (U : set β) (H : U F), f ⁻¹' U
theorem filter.map_infi_le {α : Type u} {β : Type v} {ι : Sort x} {f : ι → } {m : α → β} :
(infi f) ⨅ (i : ι), (f i)
theorem filter.map_infi_eq {α : Type u} {β : Type v} {ι : Sort x} {f : ι → } {m : α → β} (hf : f) [nonempty ι] :
(infi f) = ⨅ (i : ι), (f i)
theorem filter.map_binfi_eq {α : Type u} {β : Type v} {ι : Type w} {f : ι → } {m : α → β} {p : ι → Prop} (h : directed_on (f ⁻¹'o ge) {x : ι | p x}) (ne : ∃ (i : ι), p i) :
(⨅ (i : ι) (h : p i), f i) = ⨅ (i : ι) (h : p i), (f i)
theorem filter.map_inf_le {α : Type u} {β : Type v} {f g : filter α} {m : α → β} :
(f g) f g
theorem filter.map_inf {α : Type u} {β : Type v} {f g : filter α} {m : α → β} (h : function.injective m) :
(f g) = f g
theorem filter.map_inf' {α : Type u} {β : Type v} {f g : filter α} {m : α → β} {t : set α} (htf : t f) (htg : t g) (h : t) :
(f g) = f g
theorem filter.disjoint_map {α : Type u} {β : Type v} {m : α → β} (hm : function.injective m) {f₁ f₂ : filter α} :
disjoint f₁) f₂) disjoint f₁ f₂
theorem filter.map_eq_comap_of_inverse {α : Type u} {β : Type v} {f : filter α} {m : α → β} {n : β → α} (h₁ : m n = id) (h₂ : n m = id) :
f = f
theorem filter.map_equiv_symm {α : Type u} {β : Type v} (e : α β) (f : filter β) :
theorem filter.comap_equiv_symm {α : Type u} {β : Type v} (e : α β) (f : filter α) :
f = f
theorem filter.map_swap_eq_comap_swap {α : Type u} {β : Type v} {f : filter × β)} :
theorem filter.map_swap4_eq_comap {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} {f : filter ((α × β) × γ × δ)} :
filter.map (λ (p : × β) × γ × δ), ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) f = filter.comap (λ (p : × γ) × β × δ), ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) f

A useful lemma when dealing with uniformities.

theorem filter.le_map {α : Type u} {β : Type v} {f : filter α} {m : α → β} {g : filter β} (h : ∀ (s : set α), s fm '' s g) :
g f
theorem filter.le_map_iff {α : Type u} {β : Type v} {f : filter α} {m : α → β} {g : filter β} :
g f ∀ (s : set α), s fm '' s g
@[protected]
theorem filter.push_pull {α : Type u} {β : Type v} (f : α → β) (F : filter α) (G : filter β) :
(F G) = F G
@[protected]
theorem filter.push_pull' {α : Type u} {β : Type v} (f : α → β) (F : filter α) (G : filter β) :
G F) = G F
theorem filter.singleton_mem_pure {α : Type u} {a : α} :
{a}
theorem filter.pure_injective {α : Type u} :
@[protected, instance]
def filter.pure_ne_bot {α : Type u} {a : α} :
@[simp]
theorem filter.le_pure_iff {α : Type u} {f : filter α} {a : α} :
{a} f
theorem filter.mem_seq_def {α : Type u} {β : Type v} {f : filter (α → β)} {g : filter α} {s : set β} :
s f.seq g ∃ (u : set (α → β)) (H : u f) (t : set α) (H : t g), ∀ (x : α → β), x u∀ (y : α), y tx y s
theorem filter.mem_seq_iff {α : Type u} {β : Type v} {f : filter (α → β)} {g : filter α} {s : set β} :
s f.seq g ∃ (u : set (α → β)) (H : u f) (t : set α) (H : t g), u.seq t s
theorem filter.mem_map_seq_iff {α : Type u} {β : Type v} {γ : Type w} {f : filter α} {g : filter β} {m : α → β → γ} {s : set γ} :
s f).seq g ∃ (t : set β) (u : set α), t g u f ∀ (x : α), x u∀ (y : β), y tm x y s
theorem filter.seq_mem_seq {α : Type u} {β : Type v} {f : filter (α → β)} {g : filter α} {s : set (α → β)} {t : set α} (hs : s f) (ht : t g) :
s.seq t f.seq g
theorem filter.le_seq {α : Type u} {β : Type v} {f : filter (α → β)} {g : filter α} {h : filter β} (hh : ∀ (t : set (α → β)), t f∀ (u : set α), u gt.seq u h) :
h f.seq g
theorem filter.seq_mono {α : Type u} {β : Type v} {f₁ f₂ : filter (α → β)} {g₁ g₂ : filter α} (hf : f₁ f₂) (hg : g₁ g₂) :
f₁.seq g₁ f₂.seq g₂
@[simp]
theorem filter.pure_seq_eq_map {α : Type u} {β : Type v} (g : α → β) (f : filter α) :
.seq f = f
@[simp]
theorem filter.seq_pure {α : Type u} {β : Type v} (f : filter (α → β)) (a : α) :
f.seq = filter.map (λ (g : α → β), g a) f
@[simp]
theorem filter.seq_assoc {α : Type u} {β : Type v} {γ : Type w} (x : filter α) (g : filter (α → β)) (h : filter (β → γ)) :
h.seq (g.seq x) = .seq g).seq x
theorem filter.prod_map_seq_comm {α : Type u} {β : Type v} (f : filter α) (g : filter β) :
.seq g = (filter.map (λ (b : β) (a : α), (a, b)) g).seq f
@[protected, instance]
@[protected, instance]
@[protected, instance]
theorem filter.seq_eq_filter_seq {α β : Type l} (f : filter (α → β)) (g : filter α) :
f <*> g = f.seq g

#### `bind` equations #

@[simp]
theorem filter.eventually_bind {α : Type u} {β : Type v} {f : filter α} {m : α → } {p : β → Prop} :
(∀ᶠ (y : β) in f.bind m, p y) ∀ᶠ (x : α) in f, ∀ᶠ (y : β) in m x, p y
@[simp]
theorem filter.eventually_eq_bind {α : Type u} {β : Type v} {γ : Type w} {f : filter α} {m : α → } {g₁ g₂ : β → γ} :
g₁ =ᶠ[f.bind m] g₂ ∀ᶠ (x : α) in f, g₁ =ᶠ[m x] g₂
@[simp]
theorem filter.eventually_le_bind {α : Type u} {β : Type v} {γ : Type w} [has_le γ] {f : filter α} {m : α → } {g₁ g₂ : β → γ} :
g₁ ≤ᶠ[f.bind m] g₂ ∀ᶠ (x : α) in f, g₁ ≤ᶠ[m x] g₂
theorem filter.mem_bind' {α : Type u} {β : Type v} {s : set β} {f : filter α} {m : α → } :
s f.bind m {a : α | s m a} f
@[simp]
theorem filter.mem_bind {α : Type u} {β : Type v} {s : set β} {f : filter α} {m : α → } :
s f.bind m ∃ (t : set α) (H : t f), ∀ (x : α), x ts m x
theorem filter.bind_le {α : Type u} {β : Type v} {f : filter α} {g : α → } {l : filter β} (h : ∀ᶠ (x : α) in f, g x l) :
f.bind g l
theorem filter.bind_mono {α : Type u} {β : Type v} {f₁ f₂ : filter α} {g₁ g₂ : α → } (hf : f₁ f₂) (hg : g₁ ≤ᶠ[f₁] g₂) :
f₁.bind g₁ f₂.bind g₂
theorem filter.bind_inf_principal {α : Type u} {β : Type v} {f : filter α} {g : α → } {s : set β} :
f.bind (λ (x : α), g x = f.bind g
theorem filter.sup_bind {α : Type u} {β : Type v} {f g : filter α} {h : α → } :
(f g).bind h = f.bind h g.bind h
theorem filter.principal_bind {α : Type u} {β : Type v} {s : set α} {f : α → } :
.bind f = ⨆ (x : α) (H : x s), f x
theorem filter.sequence_mono {α : Type u} (as bs : list (filter α)) :
bssequence as sequence bs
theorem filter.mem_traverse {α' β' γ' : Type u} {f : β' → filter α'} {s : γ' → set α'} (fs : list β') (us : list γ') :
list.forall₂ (λ (b : β') (c : γ'), s c f b) fs us
theorem filter.mem_traverse_iff {α' β' : Type u} {f : β' → filter α'} (fs : list β') (t : set (list α')) :
t ∃ (us : list (set α')), list.forall₂ (λ (b : β') (s : set α'), s f b) fs us sequence us t

### Limits #

def filter.tendsto {α : Type u} {β : Type v} (f : α → β) (l₁ : filter α) (l₂ : filter β) :
Prop

`tendsto` is the generic "limit of a function" predicate. `tendsto f l₁ l₂` asserts that for every `l₂` neighborhood `a`, the `f`-preimage of `a` is an `l₁` neighborhood.

Equations
• l₁ l₂ = l₁ l₂)
theorem filter.tendsto_def {α : Type u} {β : Type v} {f : α → β} {l₁ : filter α} {l₂ : filter β} :
l₁ l₂ ∀ (s : set β), s l₂f ⁻¹' s l₁
theorem filter.tendsto_iff_eventually {α : Type u} {β : Type v} {f : α → β} {l₁ : filter α} {l₂ : filter β} :
l₁ l₂ ∀ ⦃p : β → Prop⦄, (∀ᶠ (y : β) in l₂, p y)(∀ᶠ (x : α) in l₁, p (f x))
theorem filter.tendsto.eventually {α : Type u} {β : Type v} {f : α → β} {l₁ : filter α} {l₂ : filter β} {p : β → Prop} (hf : l₁ l₂) (h : ∀ᶠ (y : β) in l₂, p y) :
∀ᶠ (x : α) in l₁, p (f x)
theorem filter.tendsto.frequently {α : Type u} {β : Type v} {f : α → β} {l₁ : filter α} {l₂ : filter β} {p : β → Prop} (hf : l₁ l₂) (h : ∃ᶠ (x : α) in l₁, p (f x)) :
∃ᶠ (y : β) in l₂, p y
theorem filter.tendsto.frequently_map {α : Type u} {β : Type v} {l₁ : filter α} {l₂ : filter β} {p : α → Prop} {q : β → Prop} (f : α → β) (c : fil