mathlib documentation

order.filter.basic

Theory of filters on sets #

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. Finally we describe a product operation filter X → filter Y → filter (X × Y).

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 α.

@[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
@[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
@[simp]
theorem filter.mem_sets {α : Type u} {f : filter α} {s : set α} :
s f.sets s f
@[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
theorem filter.ext_iff {α : Type u} {f g : filter α} :
f = g ∀ (s : set α), s f s g
@[ext]
theorem filter.ext {α : Type u} {f g : filter α} :
(∀ (s : set α), s f s g)f = g
@[simp]
theorem filter.univ_mem {α : Type u} {f : filter α} :
theorem filter.mem_of_superset {α : Type u} {f : filter α} {x y : set α} :
x fx yy f
theorem filter.inter_mem {α : Type u} {f : filter α} {s t : set α} :
s ft fs t f
@[simp]
theorem filter.inter_mem_iff {α : Type u} {f : filter α} {s t : set α} :
s t f s f 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
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 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 α} [fintype β] :
(⋂ (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)

filter_upwards [h1, ⋯, hn] replaces a goal of the form s ∈ f and terms h1 : t1 ∈ f, ⋯, hn : tn ∈ f with ∀ x, x ∈ t1 → ⋯ → x ∈ tn → x ∈ s.

filter_upwards [h1, ⋯, hn] e is a short form for { filter_upwards [h1, ⋯, hn], exact e }.

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

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

Equations
@[instance]
def filter.inhabited {α : Type u} :
Equations
@[simp]
theorem filter.mem_principal {α : Type u} {s t : set α} :
s 𝓟 t t s
theorem filter.mem_principal_self {α : Type u} (s : set α) :
s 𝓟 s
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
@[instance]
def filter.partial_order {α : Type u} :
Equations
theorem filter.le_def {α : Type u} {f g : filter α} :
f g ∀ (x : set α), x gx 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 smallest 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
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
theorem filter.mk_of_closure_sets {α : Type u} {s : set (set α)} {hs : (filter.generate s).sets = s} :

Galois insertion from sets of sets into filters.

Equations
@[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
@[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 α} :
@[instance]
def filter.complete_lattice {α : Type u} :
Equations
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.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 α)} :
(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} {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 Sup s ∀ (f : filter α), f sx 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 : ι), i IV i s i) U = ⋂ (i : ι) (H : i 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_fintype {ι : Type u_1} [fintype ι] {α : 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 α} :
f 𝓟 s s f
theorem filter.principal_mono {α : Type u} {s t : set α} :
𝓟 s 𝓟 t s t
theorem filter.monotone_principal {α : Type u} :
@[simp]
theorem filter.principal_eq_iff_eq {α : Type u} {s t : set α} :
𝓟 s = 𝓟 t s = t
@[simp]
theorem filter.join_principal_eq_Sup {α : Type u} {s : set (filter α)} :
(𝓟 s).join = Sup s
@[simp]
theorem filter.principal_univ {α : Type u} :
@[simp]
theorem filter.principal_empty {α : Type u} :

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 =
def filter.unique {α : Type u} [is_empty α] :

There is exactly one filter on an empty type. -

Equations
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 = Inf S
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.infi_sup_left {α : Type u} {ι : Sort x} {f : filter α} {g : ι → filter α} :
(⨅ (x : ι), f g x) = f infi g
theorem filter.infi_sup_right {α : Type u} {ι : Sort x} {f : filter α} {g : ι → filter α} :
(⨅ (x : ι), g x f) = infi g f
theorem filter.binfi_sup_right {α : Type u} {ι : Sort x} (p : ι → Prop) (f : ι → filter α) (g : filter α) :
(⨅ (i : ι) (h : p i), f i g) = (⨅ (i : ι) (h : p i), f i) g
theorem filter.binfi_sup_left {α : Type u} {ι : Sort x} (p : ι → Prop) (f : ι → filter α) (g : filter α) :
(⨅ (i : ι) (h : p i), g f i) = g ⨅ (i : ι) (h : p i), f i
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 sp 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.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 ip s₂p (s₁ s₂)) :
p s

principal equations #

@[simp]
theorem filter.inf_principal {α : Type u} {s t : set α} :
𝓟 s 𝓟 t = 𝓟 (s t)
@[simp]
theorem filter.sup_principal {α : Type u} {s t : set α} :
𝓟 s 𝓟 t = 𝓟 (s t)
@[simp]
theorem filter.supr_principal {α : Type u} {ι : Sort w} {s : ι → set α} :
(⨆ (x : ι), 𝓟 (s x)) = 𝓟 (⋃ (i : ι), s i)
@[simp]
theorem filter.principal_eq_bot_iff {α : Type u} {s : set α} :
@[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 f 𝓟 t {x : α | x tx s} f
theorem filter.supr_inf_principal {α : Type u} {ι : Sort x} (f : ι → filter α) (s : set α) :
(⨆ (i : ι), f i 𝓟 s) = (⨆ (i : ι), f i) 𝓟 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 𝓟 s = ) :
s f
theorem filter.diff_mem_inf_principal_compl {α : Type u} {f : filter α} {s : set α} (hs : s f) (t : set α) :
s \ t f 𝓟 t
theorem filter.principal_le_iff {α : Type u} {s : set α} {f : filter α} :
𝓟 s f ∀ (V : set α), V fs V
@[simp]
theorem filter.infi_principal_finset {α : Type u} {ι : Type w} (s : finset ι) (f : ι → set α) :
(⨅ (i : ι) (H : i s), 𝓟 (f i)) = 𝓟 (⋂ (i : ι) (H : i s), f i)
@[simp]
theorem filter.infi_principal_fintype {α : Type u} {ι : Type w} [fintype ι] (f : ι → set α) :
(⨅ (i : ι), 𝓟 (f i)) = 𝓟 (⋂ (i : ι), f i)
theorem filter.infi_principal_finite {α : Type u} {ι : Type w} {s : set ι} (hs : s.finite) (f : ι → set α) :
(⨅ (i : ι) (H : i s), 𝓟 (f i)) = 𝓟 (⋂ (i : ι) (H : i s), f i)
theorem filter.join_mono {α : Type u} {f₁ f₂ : filter (filter α)} (h : f₁ f₂) :
f₁.join f₂.join

Eventually #

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
theorem filter.eventually_iff {α : Type u} {f : filter α} {P : α → Prop} :
(∀ᶠ (x : α) in f, P x) {x : α | P x} f
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
theorem filter.eventually.and {α : Type u} {p q : α → Prop} {f : filter α} :
filter.eventually p ffilter.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
@[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} [fintype ι] {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)
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 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)
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 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 Sup fs, p x) ∀ (f : filter α), f fs(∀ᶠ (x : α) in f, p x)
@[simp]
theorem filter.eventually_supr {α : Type u} {β : Type v} {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 𝓟 a, 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 f 𝓟 s, p x) ∀ᶠ (x : α) in f, x sp x

Frequently #

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 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.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 𝓟 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 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

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 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 eventually_eq_set.

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
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
theorem filter.eventually_eq.symm {α : Type u} {β : Type v} {f g : α → β} {l : filter α} (H : f =ᶠ[l] g) :
g =ᶠ[l] f
theorem filter.eventually_eq.trans {α : Type u} {β : Type v} {f g h : α → β} {l : filter α} (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.div {α : Type u} {β : Type v} [group_with_zero β] {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} [group β] {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.sub {α : Type u} {β : Type v} [add_group β] {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.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 : α → β} :
theorem filter.eventually_eq_inf_principal_iff {α : Type u} {β : Type v} {F : filter α} {s : set α} {f g : α → β} :
f =ᶠ[F 𝓟 s] 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) :
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 : α → β} :
theorem filter.eventually_le.trans {α : Type u} {β : Type v} [preorder β] {l : filter α} {f g h : α → β} (H₁ : f ≤ᶠ[l] g) (H₂ : g ≤ᶠ[l] h) :
theorem filter.eventually_eq.trans_le {α : Type u} {β : Type v} [preorder β] {l : filter α} {f g h : α → β} (H₁ : f =ᶠ[l] g) (H₂ : g ≤ᶠ[l] h) :
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} [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.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
@[simp]
theorem filter.map_principal {α : Type u} {β : Type v} {s : set α} {f : α → β} :
filter.map f (𝓟 s) = 𝓟 (f '' s)
@[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

Equations
theorem filter.eventually_comap' {α : Type u} {β : Type v} {f : filter β} {φ : α → β} {p : β → Prop} (hf : ∀ᶠ (b : β) in f, p b) :
∀ᶠ (a : α) in filter.comap φ f, p (φ a)
@[simp]
theorem filter.eventually_comap {α : Type u} {β : Type v} {f : filter β} {φ : α → β} {P : α → Prop} :
(∀ᶠ (a : α) in filter.comap φ f, P a) ∀ᶠ (b : β) in f, ∀ (a : α), φ a = bP a
@[simp]
theorem filter.frequently_comap {α : Type u} {β : Type v} {f : filter β} {φ : α → β} {P : α → Prop} :
(∃ᶠ (a : α) in filter.comap φ f, P a) ∃ᶠ (b : β) in f, ∃ (a : α), φ a = b P a
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
@[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
@[instance]
Equations
@[instance]
Equations
theorem filter.pure_sets {α : Type u} (a : α) :
(pure a).sets = {s : set α | a s}
@[simp]
theorem filter.mem_pure {α : Type u} {a : α} {s : set α} :
s pure a a s
@[simp]
theorem filter.eventually_pure {α : Type u} {a : α} {p : α → Prop} :
(∀ᶠ (x : α) in pure a, p x) p a
@[simp]
theorem filter.principal_singleton {α : Type u} (a : α) :
𝓟 {a} = pure a
@[simp]
theorem filter.map_pure {α : Type u} {β : Type v} (f : α → β) (a : α) :
filter.map f (pure a) = pure (f a)
@[simp]
theorem filter.join_pure {α : Type u} (f : filter α) :
(pure f).join = f
@[simp]
theorem filter.pure_bind {α : Type u} {β : Type v} (a : α) (m : α → filter β) :
(pure a).bind m = m a

The monad structure on filters.

Equations
@[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.comap_id {α : Type u} {f : filter α} :
theorem filter.comap_const_of_not_mem {α : Type u} {x : α} {f : filter α} {V : set α} (hV : V f) (hx : x V) :
filter.comap (λ (y : α), x) f =
theorem filter.comap_const_of_mem {α : Type u} {x : α} {f : filter α} (h : ∀ (V : set α), V fx V) :
filter.comap (λ (y : α), x) f =
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 δ) :
@[simp]
theorem filter.comap_principal {α : Type u} {β : Type v} {m : α → β} {t : set β} :
@[simp]
theorem filter.comap_pure {α : Type u} {β : Type v} {m : α → β} {b : β} :
filter.comap m (pure b) = 𝓟 (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.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.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 (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) :
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 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 : 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.le_of_map_le_map_inj' {α : Type u} {β : Type v} {f g : filter α} {m : α → β} {s : set α} (hsf : s f) (hsg : s g) (hm : ∀ (x : α), x s∀ (y : α), y sm x = m yx = y) (h : filter.map m f filter.map m g) :
f g
theorem filter.le_of_map_le_map_inj_iff {α : Type u} {β : Type v} {f g : filter α} {m : α → β} {s : set α} (hsf : s f) (hsg : s g) (hm : ∀ (x : α), x s∀ (y : α), y sm x = m yx = y) :
theorem filter.eq_of_map_eq_map_inj' {α : Type u} {β : Type v} {f g : filter α} {m : α → β} {s : set α} (hsf : s f) (hsg : s g) (hm : ∀ (x : α), x s∀ (y : α), y sm x = m yx = y) (h : filter.map m f = filter.map m g) :
f = g
theorem filter.map_inj {α : Type u} {β : Type v} {f g : filter α} {m : α → β} (hm : function.injective m) (h : filter.map m f = filter.map m g) :
f = g
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 : α → β} :
(filter.comap m f).ne_bot ∃ᶠ (y : β) in f, y set.range m
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 : 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 𝓟 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 : α → β) :
@[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 : α → β} {t : set α} (htf : t f) (htg : t g) (h : ∀ (x : α), x t∀ (y : α), y tm x = m yx = y) :
theorem filter.map_inf {α : Type u} {β : Type v} {f g : filter α} {m : α → β} (h : function.injective m) :
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.map_swap_eq_comap_swap {α : Type u} {β : Type v} {f : filter × β)} :
theorem filter.le_map {α : Type u} {β : Type v} {f : filter α} {m : α → β} {g : filter β} (h : ∀ (s : set α), s fm '' s g) :
theorem filter.push_pull {α : Type u} {β : Type v} (f : α → β) (F : filter α) (G : filter β) :
theorem filter.push_pull' {α : Type u} {β : Type v} (f : α → β) (F : filter α) (G : filter β) :
theorem filter.singleton_mem_pure {α : Type u} {a : α} :
{a} pure a
@[instance]
def filter.pure_ne_bot {α : Type u} {a : α} :
@[simp]
theorem filter.le_pure_iff {α : Type u} {f : filter α} {a : α} :
f pure 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 (filter.map m 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 α) :
(pure g).seq f = filter.map g f
@[simp]
theorem filter.seq_pure {α : Type u} {β : Type v} (f : filter (α → β)) (a : α) :
f.seq (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
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 ts 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 𝓟 s) = f.bind g 𝓟 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 β} :
(𝓟 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 ustraverse s us traverse f fs
theorem filter.mem_traverse_iff {α' β' : Type u} {f : β' → filter α'} (fs : list β') (t : set (list α')) :
t 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 xq (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 tendsto_iff_comap.

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 α} :
x yfilter.tendsto id x y
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
@[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₁ yfilter.tendsto f x₂ yfilter.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
@[simp]
theorem filter.tendsto_principal {α : Type u} {β : Type v} {f : α → β} {l : filter α} {s : set β} :
filter.tendsto f l (𝓟 s) ∀ᶠ (a : α) in l, f a s
@[simp]
theorem filter.tendsto_principal_principal {α : Type u} {β : Type v} {f : α → β} {s : set α} {t : set β} :
filter.tendsto f (𝓟 s) (𝓟 t) ∀ (a : α), a sf a t
@[simp]
theorem filter.tendsto_pure {α : Type u} {β : Type v} {f : α → β} {a : filter α} {b : β} :
filter.tendsto f a (pure b) ∀ᶠ (x : α) in a, f x = b
theorem filter.tendsto_pure_pure {α : Type u} {β : Type v} (f : α → β) (a : α) :
filter.tendsto f (pure a) (pure (f a))
theorem filter.tendsto_const_pure {α : Type u} {β : Type v} {a : filter α} {b : β} :
filter.tendsto (λ (x : α), b) a (pure b)
theorem filter.pure_le_iff {α : Type u} {a : α} {l : filter α} :
pure a l ∀ (s : set α), s la s
theorem filter.tendsto_pure_left {α : Type u} {β : Type v} {f : α → β} {a : α} {l : filter β} :
filter.tendsto f (pure a) l ∀ (s : set β), s lf 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.

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₁ 𝓟 {x : α | p x}) l₂) (h₁ : filter.tendsto g (l₁ 𝓟 {x : α | ¬p x}) l₂) :
filter.tendsto (λ (x : α), ite (p x) (f x) (g x)) l₁ l₂
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₁ 𝓟 s) l₂) (h₁ : filter.tendsto g (l₁ 𝓟 s) l₂) :
filter.tendsto (s.piecewise f g) l₁ l₂

Products of filters #

def