mathlib3 documentation

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 #

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:

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:

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 #

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.

@[simp]
theorem filter.mem_principal {α : Type u} {s t : set α} :
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 : filter α | s t} f
@[protected, instance]
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 α} :
theorem filter.mem_generate_iff {α : Type u} {s : set (set α)} {U : set α} :
U filter.generate s (t : set (set α)) (H : t s), t.finite ⋂₀ t U
@[protected]
def filter.mk_of_closure {α : Type u} (s : set (set α)) (hs : (filter.generate s).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

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]
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.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 : ι filter α} :
(supr f).sets = (i : ι), (f i).sets
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 has_Sup.Sup s (f : filter α), f s x f
@[simp]
theorem filter.mem_supr {α : Type u} {ι : Sort x} {x : set α} {f : ι filter α} :
x supr f (i : ι), x f i
@[simp]
theorem filter.supr_ne_bot {α : Type u} {ι : Sort x} {f : ι filter α} :
( (i : ι), f i).ne_bot (i : ι), (f i).ne_bot
theorem filter.infi_eq_generate {α : Type u} {ι : Sort x} (s : ι filter α) :
infi s = filter.generate ( (i : ι), (s i).sets)
theorem filter.mem_infi_of_mem {α : Type u} {ι : Sort x} {f : ι filter α} (i : ι) {s : set α} :
s f i (s (i : ι), f i)
theorem filter.mem_infi_of_Inter {α : Type u} {ι : Type u_1} {s : ι filter α} {U : set α} {I : set ι} (I_fin : I.finite) {V : I set α} (hV : (i : I), V i s i) (hU : ( (i : I), V i) U) :
U (i : ι), s i
theorem filter.mem_infi {α : Type u} {ι : Type u_1} {s : ι filter α} {U : set α} :
(U (i : ι), s i) (I : set ι), I.finite (V : I set α), ( (i : I), V i s i) U = (i : I), V i
theorem filter.mem_infi' {α : Type u} {ι : Type u_1} {s : ι filter α} {U : set α} :
(U (i : ι), s i) (I : set ι), I.finite (V : ι set α), ( (i : ι), V i s i) ( (i : ι), i 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 : ι filter α} {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 : ι filter α} (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 α} :
theorem filter.Iic_principal {α : Type u} (s : set α) :
set.Iic (filter.principal s) = {l : filter α | s l}
@[simp]
theorem filter.principal_eq_iff_eq {α : Type u} {s t : set α} :
@[simp]
theorem filter.generate_eq_binfi {α : Type u} (S : set (set α)) :
filter.generate S = (s : set α) (H : s S), filter.principal 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 α} :
disjoint f g (s : set α) (H : s f) (t : set α) (H : t g), disjoint s t
theorem filter.disjoint_of_disjoint_of_mem {α : Type u} {f g : filter α} {s t : set α} (h : disjoint s t) (hs : s f) (ht : t g) :
theorem filter.ne_bot.not_disjoint {α : Type u} {f : filter α} {s t : set α} (hf : f.ne_bot) (hs : s f) (ht : t f) :
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 : ι filter α} (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 : ι filter α} {t : set ι} (hd : t.pairwise_disjoint l) (ht : t.finite) :
(s : ι set α), ( (i : ι), s i l i) t.pairwise_disjoint s
@[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) :
theorem filter.eq_infi_of_mem_iff_exists_mem {α : Type u} {ι : Sort x} {f : ι filter α} {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 : ι filter α} {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 : ι filter α} (h : directed ge f) [ne : nonempty ι] :
(infi f).sets = (i : ι), (f i).sets
theorem filter.mem_infi_of_directed {α : Type u} {ι : Sort x} {f : ι filter α} (h : directed ge f) [nonempty ι] (s : set α) :
s infi f (i : ι), s f i
theorem filter.mem_binfi_of_directed {α : Type u} {β : Type v} {f : β filter α} {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 : β filter α} {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 : ι filter α) :
( (i : ι), f i).sets = (t : finset ι), ( (i : ι) (H : i t), f i).sets
theorem filter.infi_sets_eq_finite' {α : Type u} {ι : Sort x} (f : ι filter α) :
( (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 : ι filter α} (s : set α) :
s infi f (t : finset ι), s (i : ι) (H : i t), f i
theorem filter.mem_infi_finite' {α : Type u} {ι : Sort x} {f : ι filter α} (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
theorem filter.mem_infi_finset {α : Type u} {β : Type v} {s : finset α} {f : α filter β} {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 : ι filter α} [nonempty ι] (hd : directed ge 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 : ι filter α} [hn : nonempty α] (hd : directed ge 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 : directed_on ge s) (hbot : s) :
theorem filter.Inf_ne_bot_of_directed {α : Type u} [nonempty α] {s : set (filter α)} (hd : directed_on ge s) (hbot : s) :
theorem filter.infi_ne_bot_iff_of_directed' {α : Type u} {ι : Sort x} {f : ι filter α} [nonempty ι] (hd : directed ge f) :
(infi f).ne_bot (i : ι), (f i).ne_bot
theorem filter.infi_ne_bot_iff_of_directed {α : Type u} {ι : Sort x} {f : ι filter α} [nonempty α] (hd : directed ge f) :
(infi f).ne_bot (i : ι), (f i).ne_bot
theorem filter.infi_sets_induct {α : Type u} {ι : Sort x} {f : ι filter α} {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]
@[simp]
@[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 α} :
@[simp]

Alias of the reverse direction of filter.principal_ne_bot_iff.

theorem filter.mem_inf_principal' {α : Type u} {f : filter α} {s t : set α} :
theorem filter.mem_inf_principal {α : Type u} {f : filter α} {s t : set α} :
s f filter.principal t {x : α | x t x s} f
theorem filter.supr_inf_principal {α : Type u} {ι : Sort x} (f : ι filter α) (s : set α) :
( (i : ι), f i filter.principal s) = ( (i : ι), f i) filter.principal s
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 : f filter.principal s = ) :
s f
theorem filter.diff_mem_inf_principal_compl {α : Type u} {f : filter α} {s : set α} (hs : s f) (t : set α) :
theorem filter.principal_le_iff {α : Type u} {s : set α} {f : filter α} :
filter.principal s f (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
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 α} :
filter.eventually p f filter.eventually q f (∀ᶠ (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 has_Sup.Sup fs, p x) (f : filter α), f fs (∀ᶠ (x : α) in f, p x)
@[simp]
theorem filter.eventually_supr {α : Type u} {ι : Sort x} {p : α Prop} {fs : ι filter α} :
(∀ᶠ (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 filter.principal a, 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 f filter.principal s, 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 filter.principal a, 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 has_Sup.Sup fs, p x) (f : filter α) (H : f fs), ∃ᶠ (x : α) in f, p x
@[simp]
theorem filter.frequently_supr {α : Type u} {β : Type v} {p : α Prop} {fs : β filter α} :
(∃ᶠ (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 α} :
theorem filter.eventually_eq.exists_mem {α : Type u} {β : Type v} {l : filter α} {f g : α β} (h : f =ᶠ[l] g) :
(s : set α) (H : s l), set.eq_on f g s
theorem filter.eventually_eq_of_mem {α : Type u} {β : Type v} {l : filter α} {f g : α β} {s : set α} (hs : s l) (h : set.eq_on f 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), set.eq_on f 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} [has_vadd 𝕜 β] {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} [has_smul 𝕜 β] {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} [has_vadd 𝕜 β] {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} [has_smul 𝕜 β] {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 : α β} :
theorem filter.eventually_eq_inf_principal_iff {α : Type u} {β : Type v} {F : filter α} {s : set α} {f g : α β} :
f =ᶠ[F filter.principal s] 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} [partial_order β] {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} [partial_order β] {l : filter α} {f g : α β} :
f =ᶠ[l] g f ≤ᶠ[l] g g ≤ᶠ[l] f
theorem filter.eventually_le.le_iff_eq {α : Type u} {β : Type v} [partial_order β] {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} [partial_order β] [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} [partial_order β] [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} [partial_order β] [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} [mul_zero_class β] [partial_order β] [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 β] [covariant_class β β has_add.add has_le.le] [covariant_class β β (function.swap has_add.add) has_le.le] {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 β] [covariant_class β β has_mul.mul has_le.le] [covariant_class β β (function.swap has_mul.mul) has_le.le] {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} [ordered_semiring β] {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} [semilattice_sup β] {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} [semilattice_sup β] {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} [semilattice_sup β] {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} [semilattice_sup β] {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 filter.map m 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 filter.map m f, P b) ∃ᶠ (a : α) in f, P (m a)
@[simp]
theorem filter.mem_map {α : Type u} {β : Type v} {f : filter α} {m : α β} {t : set β} :
theorem filter.mem_map' {α : Type u} {β : Type v} {f : filter α} {m : α β} {t : set β} :
t filter.map m 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 filter.map m f
theorem filter.image_mem_map_iff {α : Type u} {β : Type v} {f : filter α} {m : α β} {s : set α} (hf : function.injective m) :
m '' s filter.map m f s f
theorem filter.range_mem_map {α : Type u} {β : Type v} {f : filter α} {m : α β} :
theorem filter.mem_map_iff_exists_image {α : Type u} {β : Type v} {f : filter α} {m : α β} {t : set β} :
t filter.map m f (s : set α) (H : s f), m '' s t
@[simp]
theorem filter.map_id {α : Type u} {f : filter α} :
@[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' : β γ} :
@[simp]
theorem filter.map_map {α : Type u} {β : Type v} {γ : Type w} {f : filter α} {m : α β} {m' : β γ} :
theorem filter.map_congr {α : Type u} {β : Type v} {m₁ m₂ : α β} {f : filter α} (h : m₁ =ᶠ[f] m₂) :
filter.map m₁ f = filter.map m₂ 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 filter.comap f 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 filter.comap (prod.mk x) 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 filter.comap f 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 filter.comap f 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 α} :
theorem filter.compl_mem_comap {α : Type u} {β : Type v} {f : α β} {l : filter β} {s : set α} :
def filter.bind {α : Type u} {β : Type v} (f : filter α) (m : α filter β) :

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 : α) :
(has_pure.pure a).sets = {s : set α | a s}
@[simp]
theorem filter.mem_pure {α : Type u} {a : α} {s : set α} :
@[simp]
theorem filter.eventually_pure {α : Type u} {a : α} {p : α Prop} :
(∀ᶠ (x : α) in has_pure.pure a, 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 α) :
@[simp]
theorem filter.pure_bind {α : Type u} {β : Type v} (a : α) (m : α filter β) :
(has_pure.pure a).bind m = m a
@[protected]

The monad structure on filters.

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

map and comap equations #

@[simp]
theorem filter.mem_comap {α : Type u} {β : Type v} {g : filter β} {m : α β} {s : set α} :
s filter.comap m 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) :
theorem filter.eventually.comap {α : Type u} {β : Type v} {g : filter β} {p : β Prop} (hf : ∀ᶠ (b : β) in g, p b) (f : α β) :
∀ᶠ (a : α) in filter.comap f g, p (f a)
theorem filter.comap_id {α : Type u} {f : filter α} :
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 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 g x 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 = has_pure.pure c
theorem filter.comap_comap {α : Type u} {β : Type v} {γ : Type w} {f : filter α} {m : γ β} {n : β α} :

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 α) :
theorem filter.comap_comm {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} {φ : α β} {θ : α γ} {ψ : β δ} {ρ : γ δ} (H : ψ φ = ρ θ) (G : filter δ) :
theorem function.semiconj.filter_map {α : Type u} {β : Type v} {f : α β} {ga : α α} {gb : β β} (h : function.semiconj f ga gb) :
theorem function.semiconj.filter_comap {α : Type u} {β : Type v} {f : α β} {ga : α α} {gb : β β} (h : function.semiconj f ga gb) :
@[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 : α β} :
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 : α β} :
filter.map m (f₁ f₂) = filter.map m f₁ filter.map m f₂
@[simp]
theorem filter.map_supr {α : Type u} {β : Type v} {ι : Sort x} {m : α β} {f : ι filter α} :
filter.map m ( (i : ι), f i) = (i : ι), filter.map m (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 : α β} :
filter.comap m (g₁ g₂) = filter.comap m g₁ filter.comap m g₂
@[simp]
theorem filter.comap_infi {α : Type u} {β : Type v} {ι : Sort x} {m : α β} {f : ι filter β} :
filter.comap m ( (i : ι), f i) = (i : ι), filter.comap m (f i)
theorem filter.le_comap_top {α : Type u} {β : Type v} (f : α β) (l : filter α) :
theorem filter.map_comap_le {α : Type u} {β : Type v} {g : filter β} {m : α β} :
theorem filter.le_comap_map {α : Type u} {β : Type v} {f : filter α} {m : α β} :
@[simp]
theorem filter.comap_bot {α : Type u} {β : Type v} {m : α β} :
theorem filter.ne_bot_of_comap {α : Type u} {β : Type v} {g : filter β} {m : α β} (h : (filter.comap m g).ne_bot) :
theorem filter.comap_inf_principal_range {α : Type u} {β : Type v} {g : filter β} {m : α β} :
theorem filter.disjoint_comap {α : Type u} {β : Type v} {g₁ g₂ : filter β} {m : α β} (h : disjoint g₁ g₂) :
theorem filter.comap_supr {α : Type u} {β : Type v} {ι : Sort u_1} {f : ι filter β} {m : α β} :
filter.comap m (supr f) = (i : ι), filter.comap m (f i)
theorem filter.comap_Sup {α : Type u} {β : Type v} {s : set (filter β)} {m : α β} :
filter.comap m (has_Sup.Sup s) = (f : filter β) (H : f s), filter.comap m f
theorem filter.comap_sup {α : Type u} {β : Type v} {g₁ g₂ : filter β} {m : α β} :
filter.comap m (g₁ g₂) = filter.comap m g₁ filter.comap m g₂
theorem filter.map_comap {α : Type u} {β : Type v} (f : filter β) (m : α β) :
theorem filter.map_comap_of_mem {α : Type u} {β : Type v} {f : filter β} {m : α β} (hf : set.range m f) :
@[protected, instance]
def filter.can_lift {α : Type u} {β : Type v} (c : out_param α)) (p : out_param Prop)) [can_lift α β c p] :
can_lift (filter α) (filter β) (filter.map c) (λ (f : filter α), ∀ᶠ (x : α) in f, p x)
Equations
theorem filter.comap_le_comap_iff {α : Type u} {β : Type v} {f g : filter β} {m : α β} (hf : set.range m f) :
theorem filter.map_comap_of_surjective {α : Type u} {β : Type v} {f : α β} (hf : function.surjective f) (l : filter β) :
theorem function.surjective.filter_map_top {α : Type u} {β : Type v} {f : α β} (hf : function.surjective f) :
theorem filter.image_mem_of_mem_comap {α : Type u} {β : Type v} {f : filter α} {c : β α} (h : set.range c f) {W : set β} (W_in : W filter.comap c 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 filter.comap coe f) :
coe '' W f
theorem filter.comap_map {α : Type u} {β : Type v} {f : filter α} {m : α β} (h : function.injective m) :
theorem filter.mem_comap_iff {α : Type u} {β : Type v} {f : filter β} {m : α β} (inj : function.injective m) (large : set.range m f) {S : set α} :
S filter.comap m 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 : set.inj_on f s) :
filter.map f l₁ filter.map f l₂ l₁ l₂
theorem filter.map_le_map_iff {α : Type u} {β : Type v} {f g : filter α} {m : α β} (hm : function.injective m) :
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 : set.inj_on m s) :
theorem filter.map_inj {α : Type u} {β : Type v} {f g : filter α} {m : α β} (hm : function.injective m) :
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 : α β} :
(filter.comap 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)) :
theorem filter.comap_ne_bot_iff_frequently {α : Type u} {β : Type v} {f : filter β} {m : α β} :
theorem filter.comap_ne_bot_iff_compl_range {α : Type u} {β : Type v} {f : filter β} {m : α β} :
theorem filter.comap_eq_bot_iff_compl_range {α : Type u} {β : Type v} {f : filter β} {m : α β} :
theorem filter.comap_surjective_eq_bot {α : Type u} {β : Type v} {f : filter β} {m : α β} (hm : function.surjective m) :
theorem filter.disjoint_comap_iff {α : Type u} {β : Type v} {g₁ g₂ : filter β} {m : α β} (h : function.surjective m) :
disjoint (filter.comap m g₁) (filter.comap m g₂) disjoint g₁ g₂
theorem filter.ne_bot.comap_of_range_mem {α : Type u} {β : Type v} {f : filter β} {m : α β} (hf : f.ne_bot) (hm : set.range m f) :
@[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)} :
(filter.comap (function.eval 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] :
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 filter.principal s) :
theorem filter.ne_bot.comap_of_surj {α : Type u} {β : Type v} {f : filter β} {m : α β} (hf : f.ne_bot) (hm : function.surjective m) :
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) :
@[simp]
theorem filter.map_eq_bot_iff {α : Type u} {β : Type v} {f : filter α} {m : α β} :
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 : α β) :
theorem filter.ne_bot.of_map {α : Type u} {β : Type v} {f : filter α} {m : α β} :
@[protected, instance]
def filter.map_ne_bot {α : Type u} {β : Type v} {f : filter α} {m : α β} [hf : f.ne_bot] :
theorem filter.sInter_comap_sets {α : Type u} {β : Type v} (f : α β) (F : filter β) :
⋂₀ (filter.comap f F).sets = (U : set β) (H : U F), f ⁻¹' U
theorem filter.map_infi_le {α : Type u} {β : Type v} {ι : Sort x} {f : ι filter α} {m : α β} :
filter.map m (infi f) (i : ι), filter.map m (f i)
theorem filter.map_infi_eq {α : Type u} {β : Type v} {ι : Sort x} {f : ι filter α} {m : α β} (hf : directed ge f) [nonempty ι] :
filter.map m (infi f) = (i : ι), filter.map m (f i)
theorem filter.map_binfi_eq {α : Type u} {β : Type v} {ι : Type w} {f : ι filter α} {m : α β} {p : ι Prop} (h : directed_on (f ⁻¹'o ge) {x : ι | p x}) (ne : (i : ι), p i) :
filter.map m ( (i : ι) (h : p i), f i) = (i : ι) (h : p i), filter.map m (f i)
theorem filter.map_inf_le {α : Type u} {β : Type v} {f g : filter α} {m : α β} :
theorem filter.map_inf {α : Type u} {β : Type v} {f g : filter α} {m : α β} (h : function.injective m) :
theorem filter.map_inf' {α : Type u} {β : Type v} {f g : filter α} {m : α β} {t : set α} (htf : t f) (htg : t g) (h : set.inj_on m t) :
theorem filter.disjoint_map {α : Type u} {β : Type v} {m : α β} (hm : function.injective m) {f₁ f₂ : filter α} :
disjoint (filter.map m f₁) (filter.map m f₂) disjoint f₁ f₂
theorem filter.map_equiv_symm {α : Type u} {β : Type v} (e : α β) (f : filter β) :
theorem filter.map_eq_comap_of_inverse {α : Type u} {β : Type v} {f : filter α} {m : α β} {n : β α} (h₁ : m n = id) (h₂ : n m = id) :
theorem filter.comap_equiv_symm {α : Type u} {β : Type v} (e : α β) (f : filter α) :
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 f m '' s g) :
theorem filter.le_map_iff {α : Type u} {β : Type v} {f : filter α} {m : α β} {g : filter β} :
g filter.map m f (s : set α), s f m '' s g
@[protected]
theorem filter.push_pull {α : Type u} {β : Type v} (f : α β) (F : filter α) (G : filter β) :
@[protected]
theorem filter.push_pull' {α : Type u} {β : Type v} (f : α β) (F : filter α) (G : filter β) :
theorem filter.singleton_mem_pure {α : Type u} {a : α} :
@[protected, instance]
def filter.pure_ne_bot {α : Type u} {a : α} :
@[simp]
theorem filter.le_pure_iff {α : Type u} {f : filter α} {a : α} :
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 t x 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 (filter.map m f).seq g (t : set β) (u : set α), t g u f (x : α), x u (y : β), y t m 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 g t.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 α) :
@[simp]
theorem filter.seq_pure {α : Type u} {β : Type v} (f : filter β)) (a : α) :
f.seq (has_pure.pure a) = 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) = ((filter.map function.comp h).seq g).seq x
theorem filter.prod_map_seq_comm {α : Type u} {β : Type v} (f : filter α) (g : filter β) :
(filter.map prod.mk f).seq g = (filter.map (λ (b : β) (a : α), (a, b)) g).seq f
@[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 : α filter β} {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 : α filter β} {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 : α filter β} {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 : α filter β} :
s f.bind m {a : α | s m a} f
@[simp]
theorem filter.mem_bind {α : Type u} {β : Type v} {s : set β} {f : filter α} {m : α filter β} :
s f.bind m (t : set α) (H : t f), (x : α), x t s m x
theorem filter.bind_le {α : Type u} {β : Type v} {f : filter α} {g : α filter β} {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₂ : α filter β} (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 : α filter β} {s : set β} :
f.bind (λ (x : α), g x filter.principal s) = f.bind g filter.principal s
theorem filter.sup_bind {α : Type u} {β : Type v} {f g : filter α} {h : α filter β} :
(f g).bind h = f.bind h g.bind h
theorem filter.principal_bind {α : Type u} {β : Type v} {s : set α} {f : α filter β} :
(filter.principal s).bind f = (x : α) (H : x s), f x
theorem filter.sequence_mono {α : Type u} (as bs : list (filter α)) :
theorem filter.mem_traverse {α' β' γ' : Type u} {f : β' filter α'} {s : γ' set α'} (fs : list β') (us : list γ') :
list.forall₂ (λ (b : β') (c : γ'), s c f b) fs us traversable.traverse s us traversable.traverse f fs
theorem filter.mem_traverse_iff {α' β' : Type u} {f : β' filter α'} (fs : list β') (t : set (list α')) :
t traversable.traverse f fs (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
theorem filter.tendsto_def {α : Type u} {β : Type v} {f : α β} {l₁ : filter α} {l₂ : filter β} :
filter.tendsto f l₁ l₂ (s : set β), s l₂ f ⁻¹' s l₁
theorem filter.tendsto_iff_eventually {α : Type u} {β : Type v} {f : α β} {l₁ : filter α} {l₂ : filter β} :
filter.tendsto f 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 : filter.tendsto f 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 : filter.tendsto f 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 : filter.tendsto f l₁ l₂) (w : (x : α), p x q (f x)) (h : ∃ᶠ (x : α) in l₁, p x) :
∃ᶠ (y : β) in l₂, q y
@[simp]
theorem filter.tendsto_bot {α : Type u} {β : Type v} {f : α β} {l : filter β} :
@[simp]
theorem filter.tendsto_top {α : Type u} {β : Type v} {f : α β} {l : filter α} :
theorem filter.le_map_of_right_inverse {α : Type u} {β : Type v} {mab : α β} {mba : β α} {f : filter α} {g : filter β} (h₁ : mab mba =ᶠ[g] id) (h₂ : filter.tendsto mba g f) :
g filter.map mab f
theorem filter.tendsto_of_is_empty {α : Type u} {β : Type v} [is_empty α] {f : α β} {la : filter α} {lb : filter β} :
theorem filter.eventually_eq_of_left_inv_of_right_inv {α : Type u} {β : Type v} {f : α β} {g₁ g₂ : β α} {fa : filter α} {fb : filter β} (hleft : ∀ᶠ (x : α) in fa, g₁ (f x) = x) (hright : ∀ᶠ (y : β) in fb, f (g₂ y) = y) (htendsto : filter.tendsto g₂ fb fa) :
g₁ =ᶠ[fb] g₂
theorem filter.tendsto_iff_comap {α : Type u} {β : Type v} {f : α β} {l₁ : filter α} {l₂ : filter β} :
filter.tendsto f l₁ l₂ l₁ filter.comap f l₂
theorem filter.tendsto.le_comap {α : Type u} {β : Type v} {f : α β} {l₁ : filter α} {l₂ : filter β} :
filter.tendsto f l₁ l₂ l₁ filter.comap f l₂

Alias of the forward direction of filter.tendsto_iff_comap.

@[protected]
theorem filter.tendsto.disjoint {α : Type u} {β : Type v} {f : α β} {la₁ la₂ : filter α} {lb₁ lb₂ : filter β} (h₁ : filter.tendsto f la₁ lb₁) (hd : disjoint lb₁ lb₂) (h₂ : filter.tendsto f la₂ lb₂) :
disjoint la₁ la₂
theorem filter.tendsto_congr' {α : Type u} {β : Type v} {f₁ f₂ : α β} {l₁ : filter α} {l₂ : filter β} (hl : f₁ =ᶠ[l₁] f₂) :
filter.tendsto f₁ l₁ l₂ filter.tendsto f₂ l₁ l₂
theorem filter.tendsto.congr' {α : Type u} {β : Type v} {f₁ f₂ : α β} {l₁ : filter α} {l₂ : filter β} (hl : f₁ =ᶠ[l₁] f₂) (h : filter.tendsto f₁ l₁ l₂) :
filter.tendsto f₂ l₁ l₂
theorem filter.tendsto_congr {α : Type u} {β : Type v} {f₁ f₂ : α β} {l₁ : filter α} {l₂ : filter β} (h : (x : α), f₁ x = f₂ x) :
filter.tendsto f₁ l₁ l₂ filter.tendsto f₂ l₁ l₂
theorem filter.tendsto.congr {α : Type u} {β : Type v} {f₁ f₂ : α β} {l₁ : filter α} {l₂ : filter β} (h : (x : α), f₁ x = f₂ x) :
filter.tendsto f₁ l₁ l₂ filter.tendsto f₂ l₁ l₂
theorem filter.tendsto_id' {α : Type u} {x y : filter α} :
theorem filter.tendsto_id {α : Type u} {x : filter α} :
theorem filter.tendsto.comp {α : Type u} {β : Type v} {γ : Type w} {f : α β} {g : β γ} {x : filter α} {y : filter β} {z : filter γ} (hg : filter.tendsto g y z) (hf : filter.tendsto f x y) :
theorem filter.tendsto.mono_left {α : Type u} {β : Type v} {f : α β} {x y : filter α} {z : filter β} (hx : filter.tendsto f x z) (h : y x) :
theorem filter.tendsto.mono_right {α : Type u} {β : Type v} {f : α β} {x : filter α} {y z : filter β} (hy : filter.tendsto f x y) (hz : y z) :
theorem filter.tendsto.ne_bot {α : Type u} {β : Type v} {f : α β} {x : filter α} {y : filter β} (h : filter.tendsto f x y) [hx : x.ne_bot] :
theorem filter.tendsto_map {α : Type u} {β : Type v} {f : α β} {x : filter α} :
theorem filter.tendsto_map' {α : Type u} {β : Type v} {γ : Type w} {f : β γ} {g : α β} {x : filter α} {y : filter γ} (h : filter.tendsto (f g) x y) :
@[simp]
theorem filter.tendsto_map'_iff {α : Type u} {β : Type v} {γ : Type w} {f : β γ} {g : α β} {x : filter α} {y : filter γ} :
theorem filter.tendsto_comap {α : Type u} {β : Type v} {f : α β} {x : filter β} :
@[simp]
theorem filter.tendsto_comap_iff {α : Type u} {β : Type v} {γ : Type w} {f : α β} {g : β γ} {a : filter α} {c : filter γ} :
theorem filter.tendsto_comap'_iff {α : Type u} {β : Type v} {γ : Type w} {m : α β} {f : filter α} {g : filter β} {i : γ α} (h : set.range i f) :
theorem filter.tendsto.of_tendsto_comp {α : Type u} {β : Type v} {γ : Type w} {f : α β} {g : β γ} {a : filter α} {b : filter β} {c : filter γ} (hfg : filter.tendsto (g f) a c) (hg : filter.comap g c b) :
theorem filter.comap_eq_of_inverse {α : Type u} {β : Type v} {f : filter α} {g : filter β} {φ : α β} (ψ : β α) (eq : ψ φ = id) (hφ : filter.tendsto φ f g) (hψ : filter.tendsto ψ g f) :
theorem filter.map_eq_of_inverse {α : Type u} {β : Type v} {f : filter α} {g : filter β} {φ : α β} (ψ : β α) (eq : φ ψ = id) (hφ : filter.tendsto φ f g) (hψ : filter.tendsto ψ g f) :
filter.map φ f = g
theorem filter.tendsto_inf {α : Type u} {β : Type v} {f : α β} {x : filter α} {y₁ y₂ : filter β} :
filter.tendsto f x (y₁ y₂) filter.tendsto f x y₁ filter.tendsto f x y₂
theorem filter.tendsto_inf_left {α : Type u} {β : Type v} {f : α β} {x₁ x₂ : filter α} {y : filter β} (h : filter.tendsto f x₁ y) :
filter.tendsto f (x₁ x₂) y
theorem filter.tendsto_inf_right {α : Type u} {β : Type v} {f : α β} {x₁ x₂ : filter α} {y : filter β} (h : filter.tendsto f x₂ y) :
filter.tendsto f (x₁ x₂) y
theorem filter.tendsto.inf {α : Type u} {β : Type v} {f : α β} {x₁ x₂ : filter α} {y₁ y₂ : filter β} (h₁ : filter.tendsto f x₁ y₁) (h₂ : filter.tendsto f x₂ y₂) :
filter.tendsto f (x₁ x₂) (y₁ y₂)
@[simp]
theorem filter.tendsto_infi {α : Type u} {β : Type v} {ι : Sort x} {f : α β} {x : filter α} {y : ι filter β} :
filter.tendsto f x ( (i : ι), y i) (i : ι), filter.tendsto f x (y i)
theorem filter.tendsto_infi' {α : Type u} {β : Type v} {ι : Sort x} {f : α β} {x : ι filter α} {y : filter β} (i : ι) (hi : filter.tendsto f (x i) y) :
filter.tendsto f ( (i : ι), x i) y
theorem filter.tendsto_infi_infi {α : Type u} {β : Type v} {ι : Sort x} {f : α β} {x : ι filter α} {y : ι filter β} (h : (i : ι), filter.tendsto f (x i) (y i)) :
@[simp]
theorem filter.tendsto_sup {α : Type u} {β : Type v} {f : α β} {x₁ x₂ : filter α} {y : filter β} :
filter.tendsto f (x₁ x₂) y filter.tendsto f x₁ y filter.tendsto f x₂ y
theorem filter.tendsto.sup {α : Type u} {β : Type v} {f : α β} {x₁ x₂ : filter α} {y : filter β} :
filter.tendsto f x₁ y filter.tendsto f x₂ y filter.tendsto f (x₁ x₂) y
@[simp]
theorem filter.tendsto_supr {α : Type u} {β : Type v} {ι : Sort x} {f : α β} {x : ι filter α} {y : filter β} :
filter.tendsto f ( (i : ι), x i) y (i : ι), filter.tendsto f (x i) y
theorem filter.tendsto_supr_supr {α : Type u} {β : Type v} {ι : Sort x} {f : α β} {x : ι filter α} {y : ι filter β} (h : (i : ι), filter.tendsto f (x i) (y i)) :
@[simp]
theorem filter.tendsto_principal {α : Type u} {β : Type v} {f : α β} {l : filter α} {s : set β} :
filter.tendsto f l (filter.principal s) ∀ᶠ (a : α) in l, f a s
@[simp]
theorem filter.tendsto_principal_principal {α : Type u} {β : Type v} {f : α β} {s : set α} {t : set β} :
@[simp]
theorem filter.tendsto_pure {α : Type u} {β : Type v} {f : α β} {a : filter α} {b : β} :
filter.tendsto f a (has_pure.pure b) ∀ᶠ (x : α) in a, f x = b
theorem filter.tendsto_pure_pure {α : Type u} {β : Type v} (f : α β) (a : α) :
theorem filter.tendsto_const_pure {α : Type u} {β : Type v} {a : filter α} {b : β} :
filter.tendsto (λ (x : α), b) a (has_pure.pure b)
theorem filter.pure_le_iff {α : Type u} {a : α} {l : filter α} :
has_pure.pure a l (s : set α), s l a s
theorem filter.tendsto_pure_left {α : Type u} {β : Type v} {f : α β} {a : α} {l : filter β} :
filter.tendsto f (has_pure.pure a) l (s : set β), s l f a s
@[simp]
theorem filter.map_inf_principal_preimage {α : Type u} {β : Type v} {f : α β} {s : set β} {l : filter α} :
theorem filter.tendsto.not_tendsto {α : Type u} {β : Type v} {f : α β} {a : filter α} {b₁ b₂ : filter β} (hf : filter.tendsto f a b₁) [a.ne_bot] (hb : disjoint b₁ b₂) :

If two filters are disjoint, then a function cannot tend to both of them along a non-trivial filter.

@[protected]
theorem filter.tendsto.if {α : Type u} {β : Type v} {l₁ : filter α} {l₂ : filter β} {f g : α β} {p : α Prop} [Π (x : α), decidable (p x)] (h₀ : filter.tendsto f (l₁ filter.principal {x : α | p x}) l₂) (h₁ : filter.tendsto g (l₁ filter.principal {x : α | ¬p x}) l₂) :
filter.tendsto (λ (x : α), ite (p x) (f x) (g x)) l₁ l₂
@[protected]
theorem filter.tendsto.if' {α : Type u_1} {β : Type u_2} {l₁ : filter α} {l₂ : filter β} {f g : α β} {p : α Prop} [decidable_pred p] (hf : filter.tendsto f l₁ l₂) (hg : filter.tendsto g l₁ l₂) :
filter.tendsto (λ (a : α), ite (p a) (f a) (g a)) l₁ l₂
@[protected]
theorem filter.tendsto.piecewise {α : Type u} {β : Type v} {l₁ : filter α} {l₂ : filter β} {f g : α β} {s : set α} [Π (x : α), decidable (x s)] (h₀ : filter.tendsto f (l₁ filter.principal s) l₂) (h₁ : filter.tendsto g (l₁ filter.principal s) l₂) :
filter.tendsto (s.piecewise f g) l₁ l₂
theorem set.eq_on.eventually_eq {α : Type u_1} {β : Type u_2} {s : set α} {f g : α β} (h : set.eq_on f g s) :
theorem set.eq_on.eventually_eq_of_mem {α : Type u_1} {β : Type u_2} {s : set α} {l : filter α} {f g : α β} (h : set.eq_on f g s) (hl : s l) :
f =ᶠ[l] g
theorem has_subset.subset.eventually_le {α : Type u_1} {l : filter α} {s t : set α} (h : s t) :
theorem set.maps_to.tendsto {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {f : α β} (h : set.maps_to f s t) :