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_1Type 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

theorem filter.univ_mem_sets {α : Type u} {f : filter α} :

theorem filter.mem_sets_of_superset {α : Type u} {f : filter α} {x y : set α} :
x fx yy f

theorem filter.inter_mem_sets {α : Type u} {f : filter α} {s t : set α} :
s ft fs t f

theorem filter.univ_mem_sets' {α : Type u} {f : filter α} {s : set α} :
(∀ (a : α), a s)s f

theorem filter.mp_sets {α : Type u} {f : filter α} {s t : set α} :
s f{x : α | x sx t} ft f

theorem filter.congr_sets {α : Type u} {f : filter α} {s t : set α} :
{x : α | x s x t} f(s f t f)

theorem filter.Inter_mem_sets {α : Type u} {f : filter α} {β : Type v} {s : β → set α} {is : set β} :
is.finite(∀ (i : β), i iss i f)(⋂ (i : β) (H : i is), s i) f

theorem filter.sInter_mem_sets_of_finite {α : Type u} {f : filter α} {s : set (set α)} :
s.finite(∀ (U : set α), U sU f)⋂₀s f

theorem filter.Inter_mem_sets_of_fintype {α : Type u} {f : filter α} {β : Type v} {s : β → set α} [fintype β] :
(∀ (i : β), s i f)(⋂ (i : β), s i) f

theorem filter.exists_sets_subset_iff {α : Type u} {f : filter α} {s : set α} :
(∃ (t : set α) (H : t f), t s) s f

theorem filter.monotone_mem_sets {α : 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} :
set αfilter α

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_sets {α : 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} :
filter (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_sets {α : 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} :
set (set α)set α → Prop

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

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

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 α)) :

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
@[simp]
theorem filter.mem_inf_sets {α : Type u} {f g : filter α} {s : set α} :
s f g ∃ (t₁ : set α) (H : t₁ f) (t₂ : set α) (H : t₂ g), t₁ t₂ s

theorem filter.mem_inf_sets_of_left {α : Type u} {f g : filter α} {s : set α} :
s fs f g

theorem filter.mem_inf_sets_of_right {α : Type u} {f g : filter α} {s : set α} :
s gs f g

theorem filter.inter_mem_inf_sets {α : Type u} {f g : filter α} {s t : set α} :
s ft gs t f g

@[instance]
def filter.has_top {α : Type u} :

Equations
theorem filter.mem_top_sets_iff_forall {α : Type u} {s : set α} :
s ∀ (x : α), x s

@[simp]
theorem filter.mem_top_sets {α : Type u} {s : set α} :

@[instance]
def filter.complete_lattice {α : Type u} :

Equations
@[class]
def filter.ne_bot {α : Type u} :
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.

Equations
Instances
theorem filter.ne_bot.ne {α : Type u} {f : filter α} :
f.ne_botf

@[simp]
theorem filter.not_ne_bot {α : Type u_1} {f : filter α} :

theorem filter.ne_bot.mono {α : Type u} {f g : filter α} :
f.ne_botf g → g.ne_bot

theorem filter.ne_bot_of_le {α : Type u} {f g : filter α} [hf : f.ne_bot] :
f g → g.ne_bot

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_sets {α : Type u} {s : set α} :

@[simp]
theorem filter.mem_sup_sets {α : 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 α} :
s ft gs t f g

@[simp]
theorem filter.mem_Sup_sets {α : Type u} {x : set α} {s : set (filter α)} :
x Sup s ∀ (f : filter α), f sx f

@[simp]
theorem filter.mem_supr_sets {α : Type u} {ι : Sort x} {x : set α} {f : ι → filter α} :
x supr f ∀ (i : ι), x f i

theorem filter.infi_eq_generate {α : Type u} {ι : Sort x} (s : ι → filter α) :
infi s = filter.generate (⋃ (i : ι), (s i).sets)

theorem filter.mem_infi_iff {α : Type u} {ι : Type u_1} {s : ι → filter α} {U : set α} :
(U ⨅ (i : ι), s i) ∃ (I : set ι), I.finite ∃ (V : {i : ι | i I}set α), (∀ (i : {i : ι | i I}), V i s i) (⋂ (i : {i : ι | i I}), V i) U

@[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_in_sets_eq_bot {α : Type u} {f : filter α} :

theorem filter.nonempty_of_mem_sets {α : Type u} {f : filter α} [hf : f.ne_bot] {s : set α} :
s f → s.nonempty

theorem filter.ne_bot.nonempty_of_mem {α : Type u} {f : filter α} (hf : f.ne_bot) {s : set α} :
s f → s.nonempty

theorem filter.nonempty_of_ne_bot {α : Type u} (f : filter α) [f.ne_bot] :

theorem filter.filter_eq_bot_of_not_nonempty {α : Type u} (f : filter α) :
¬nonempty αf =

theorem filter.forall_sets_nonempty_iff_ne_bot {α : Type u} {f : filter α} :
(∀ (s : set α), s f → s.nonempty) f.ne_bot

theorem filter.mem_sets_of_eq_bot {α : Type u} {f : filter α} {s : set α} :
f 𝓟 s = s f

theorem filter.inf_ne_bot_iff {α : Type u} {f g : filter α} :
(f g).ne_bot ∀ {U V : set α}, U fV g(U V).nonempty

theorem filter.inf_principal_ne_bot_iff {α : Type u} {f : filter α} {s : set α} :
(f 𝓟 s).ne_bot ∀ (U : set α), U f(U s).nonempty

theorem filter.inf_eq_bot_iff {α : Type u} {f g : filter α} :
f g = ∃ (U V : set α), U f V g U V =

theorem filter.disjoint_iff {α : Type u} {f g : filter α} :
disjoint f g ∃ (U V : set α), U f V g U V =

theorem filter.eq_Inf_of_mem_sets_iff_exists_mem {α : Type u} {S : set (filter α)} {l : filter α} :
(∀ {s : set α}, s l ∃ (f : filter α) (H : f S), s f)l = Inf S

theorem filter.eq_infi_of_mem_sets_iff_exists_mem {α : Type u} {ι : Sort x} {f : ι → filter α} {l : filter α} :
(∀ {s : set α}, s l ∃ (i : ι), s f i)l = infi f

theorem filter.eq_binfi_of_mem_sets_iff_exists_mem {α : Type u} {ι : Sort x} {f : ι → filter α} {p : ι → Prop} {l : filter α} :
(∀ {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 {α : Type u} {ι : Sort x} {f : ι → filter α} (h : directed ge f) [nonempty ι] (s : set α) :
s infi f ∃ (i : ι), s f i

theorem filter.mem_binfi {α : 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 β} :
directed_on (f ⁻¹'o ge) ss.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_sets_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) (⋂ (a : α) (H : a s), p a) t

theorem filter.infi_ne_bot_of_directed' {α : Type u} {ι : Sort x} {f : ι → filter α} [nonempty ι] :
directed ge f(∀ (i : ι), (f i).ne_bot)(infi f).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 α] :
directed ge f(∀ (i : ι), (f i).ne_bot)(infi f).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 ι] :
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 α] :
directed ge f((infi f).ne_bot ∀ (i : ι), (f i).ne_bot)

theorem filter.mem_infi_sets {α : Type u} {ι : Sort x} {f : ι → filter α} (i : ι) {s : set α} :
s f i(s ⨅ (i : ι), f i)

theorem filter.infi_sets_induct {α : Type u} {ι : Sort x} {f : ι → filter α} {s : set α} (hs : s infi f) {p : set α → Prop} :
p set.univ(∀ {i : ι} {s₁ s₂ : set α}, s₁ f ip s₂p (s₁ s₂))(∀ {s₁ s₂ : set α}, s₁ s₂p s₁p s₂)p s

@[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 α} :

theorem filter.principal_ne_bot_iff {α : Type u} {s : set α} :

theorem filter.is_compl_principal {α : Type u} (s : set α) :

theorem filter.inf_principal_eq_bot {α : Type u} {f : filter α} {s : set α} :
s ff 𝓟 s =

theorem filter.mem_inf_principal {α : Type u} {f : filter α} {s t : set α} :
s f 𝓟 t {x : α | x tx 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.mem_iff_inf_principal_compl {α : Type u} {f : filter α} {V : set α} :

theorem filter.le_iff_forall_inf_principal_compl {α : Type u} {f g : filter α} :
f g ∀ (V : set α), V gf 𝓟 V =

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.join_mono {α : Type u} {f₁ f₂ : filter (filter α)} :
f₁ f₂f₁.join f₂.join

Eventually

def filter.eventually {α : Type u} :
(α → Prop)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 α} :
(∀ (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} :
(∀ᶠ (x : α) in f₂, p x)(∀ᶠ (x : α) in f₁, p x)

theorem filter.eventually_of_mem {α : Type u} {f : filter α} {P : α → Prop} {U : set α} :
U f(∀ (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 α} :
(∀ (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 α} [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 α} :
(∀ᶠ (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 α} :
(∀ᶠ (x : α) in f, p x)(∀ᶠ (x : α) in f, p xq x)(∀ᶠ (x : α) in f, q x)

theorem filter.eventually.mono {α : Type u} {p q : α → Prop} {f : filter α} :
(∀ᶠ (x : α) in f, p x)(∀ (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} :
(∀ᶠ (x : α) in f, p x)(∀ᶠ (x : α) in f, p x q x)(∀ᶠ (x : α) in f, q x)

theorem filter.eventually_congr {α : Type u} {f : filter α} {p q : α → Prop} :
(∀ᶠ (x : α) in f, p x q x)((∀ᶠ (x : α) in f, p x) ∀ᶠ (x : α) in f, q x)

@[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_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} :
(α → Prop)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} :
(∀ᶠ (x : α) in f, p x)(∃ᶠ (x : α) in f, p x)

theorem filter.frequently_of_forall {α : Type u} {f : filter α} [f.ne_bot] {p : α → Prop} :
(∀ (x : α), p x)(∃ᶠ (x : α) in f, p x)

theorem filter.frequently.mp {α : Type u} {p q : α → Prop} {f : filter α} :
(∃ᶠ (x : α) in f, p x)(∀ᶠ (x : α) in f, p xq x)(∃ᶠ (x : α) in f, q x)

theorem filter.frequently.mono {α : Type u} {p q : α → Prop} {f : filter α} :
(∃ᶠ (x : α) in f, p x)(∀ (x : α), p xq x)(∃ᶠ (x : α) in f, q x)

theorem filter.frequently.and_eventually {α : Type u} {p q : α → Prop} {f : filter α} :
(∃ᶠ (x : α) in f, p x)(∀ᶠ (x : α) in f, q x)(∃ᶠ (x : α) in f, p x q x)

theorem filter.frequently.exists {α : Type u} {p : α → Prop} {f : filter α} :
(∃ᶠ (x : α) in f, p x)(∃ (x : α), p x)

theorem filter.eventually.exists {α : Type u} {p : α → Prop} {f : filter α} [f.ne_bot] :
(∀ᶠ (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_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

theorem filter.inf_ne_bot_iff_frequently_left {α : Type u} {f g : filter α} :
(f g).ne_bot ∀ {p : α → Prop}, (∀ᶠ (x : α) in f, p x)(∃ᶠ (x : α) in g, p x)

theorem filter.inf_ne_bot_iff_frequently_right {α : Type u} {f g : filter α} :
(f g).ne_bot ∀ {p : α → Prop}, (∀ᶠ (x : α) in g, p x)(∃ᶠ (x : α) in f, 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} :
filter α(α → β)(α → β) → 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 : α → β} :
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) :
(∀ᶠ (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 : α → β} :
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 α} :
s lset.eq_on f g sf =ᶠ[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 : α → β} :
f =ᶠ[l] gl' lf =ᶠ[l'] g

theorem filter.eventually_eq.refl {α : Type u} {β : Type v} (l : filter α) (f : α → β) :
f =ᶠ[l] f

theorem filter.eventually_eq.symm {α : Type u} {β : Type v} {f g : α → β} {l : filter α} :
f =ᶠ[l] gg =ᶠ[l] f

theorem filter.eventually_eq.trans {α : Type u} {β : Type v} {f g h : α → β} {l : filter α} :
f =ᶠ[l] gg =ᶠ[l] hf =ᶠ[l] h

theorem filter.eventually_eq.prod_mk {α : Type u} {β : Type v} {γ : Type w} {l : filter α} {f f' : α → β} (hf : f =ᶠ[l] f') {g g' : α → γ} :
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 : β → γ → δ) :
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 α} :
f =ᶠ[l] gf' =ᶠ[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 α} :
f =ᶠ[l] gf' =ᶠ[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 α} :
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 α} :
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 α} :
f =ᶠ[l] gf' =ᶠ[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 α} :
f =ᶠ[l] gf' =ᶠ[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 α} :
s =ᶠ[l] ts' =ᶠ[l] t's s' =ᶠ[l] t t'

theorem filter.eventually_eq.union {α : Type u} {s t s' t' : set α} {l : filter α} :
s =ᶠ[l] ts' =ᶠ[l] t's s' =ᶠ[l] t t'

theorem filter.eventually_eq.compl {α : Type u} {s t : set α} {l : filter α} :
s =ᶠ[l] ts =ᶠ[l] t

theorem filter.eventually_eq.diff {α : Type u} {s t s' t' : set α} {l : filter α} :
s =ᶠ[l] ts' =ᶠ[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

@[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

def filter.eventually_le {α : Type u} {β : Type v} [has_le β] :
filter α(α → β)(α → β) → 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' : α → β} :
f ≤ᶠ[l] gf =ᶠ[l] f'g =ᶠ[l] g'f' ≤ᶠ[l] g'

theorem filter.eventually_le_congr {α : Type u} {β : Type v} [has_le β] {l : filter α} {f f' g g' : α → β} :
f =ᶠ[l] f'g =ᶠ[l] g'(f ≤ᶠ[l] g f' ≤ᶠ[l] g')

theorem filter.eventually_eq.le {α : Type u} {β : Type v} [preorder β] {l : filter α} {f g : α → β} :
f =ᶠ[l] gf ≤ᶠ[l] g

theorem filter.eventually_le.refl {α : Type u} {β : Type v} [preorder β] (l : filter α) (f : α → β) :

theorem filter.eventually_le.trans {α : Type u} {β : Type v} [preorder β] {l : filter α} {f g h : α → β} :
f ≤ᶠ[l] gg ≤ᶠ[l] hf ≤ᶠ[l] h

theorem filter.eventually_eq.trans_le {α : Type u} {β : Type v} [preorder β] {l : filter α} {f g h : α → β} :
f =ᶠ[l] gg ≤ᶠ[l] hf ≤ᶠ[l] h

theorem filter.eventually_le.trans_eq {α : Type u} {β : Type v} [preorder β] {l : filter α} {f g h : α → β} :
f ≤ᶠ[l] gg =ᶠ[l] hf ≤ᶠ[l] h

theorem filter.eventually_le.antisymm {α : Type u} {β : Type v} [partial_order β] {l : filter α} {f g : α → β} :
f ≤ᶠ[l] gg ≤ᶠ[l] ff =ᶠ[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 : α → β} :
f ≤ᶠ[l] g(g ≤ᶠ[l] f g =ᶠ[l] f)

theorem filter.join_le {α : Type u} {f : filter (filter α)} {l : filter α} :
(∀ᶠ (m : filter α) in f, m l)f.join l

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

def filter.map {α : Type u} {β : Type v} :
(α → β)filter α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 β} :
t filter.map m f {x : α | m x t} f

theorem filter.image_mem_map {α : Type u} {β : Type v} {f : filter α} {m : α → β} {s : set α} :
s fm '' s filter.map m f

theorem filter.range_mem_map {α : Type u} {β : Type v} {f : filter α} {m : α → β} :

theorem filter.mem_map_sets_iff {α : 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_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 α} :
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} :
(α → β)filter βfilter α

The inverse map of a filter

Equations
@[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} :
filter α(α → filter β)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} :
filter (α → β)filter α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_sets {α : 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

@[simp]
theorem filter.mem_comap_sets {α : 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 β} :
t gm ⁻¹' t filter.comap m g

theorem filter.comap_id {α : Type u} {f : filter α} :

theorem filter.comap_const_of_not_mem {α : Type u} {x : α} {f : filter α} {V : set α} :
V fx Vfilter.comap (λ (y : α), x) f =

theorem filter.comap_const_of_mem {α : Type u} {x : α} {f : filter α} :
(∀ (V : set α), V fx V)filter.comap (λ (y : α), x) f =

theorem filter.comap_comap {α : Type u} {β : Type v} {γ : Type w} {f : filter α} {m : γ → β} {n : β → α} :

@[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.image_mem_sets {α : Type u} {β : Type v} {f : filter α} {c : β → α} (h : set.range c f) {W : set β} :
W filter.comap c fc '' W f

theorem filter.image_coe_mem_sets {α : Type u} {f : filter α} {U : set α} (h : U f) {W : set U} :

theorem filter.comap_map {α : Type u} {β : Type v} {f : filter α} {m : α → β} :

theorem filter.le_of_map_le_map_inj' {α : Type u} {β : Type v} {f g : filter α} {m : α → β} {s : set α} :
s fs g(∀ (x : α), x s∀ (y : α), y sm x = m yx = y)filter.map m f filter.map m gf g

theorem filter.le_of_map_le_map_inj_iff {α : Type u} {β : Type v} {f g : filter α} {m : α → β} {s : set α} :
s fs g(∀ (x : α), x s∀ (y : α), y sm x = m yx = y)(filter.map m f filter.map m g f g)

theorem filter.eq_of_map_eq_map_inj' {α : Type u} {β : Type v} {f g : filter α} {m : α → β} {s : set α} :
s fs g(∀ (x : α), x s∀ (y : α), y sm x = m yx = y)filter.map m f = filter.map m gf = g

theorem filter.map_inj {α : Type u} {β : Type v} {f g : filter α} {m : α → β} :
(∀ (x y : α), m x = m yx = y)filter.map m f = filter.map m gf = g

theorem filter.le_map_comap_of_surjective' {α : Type u} {β : Type v} {f : α → β} {l : filter β} {u : set β} :
u l(∀ (y : β), y u(∃ (x : α), f x = y))l filter.map f (filter.comap f l)

theorem filter.map_comap_of_surjective' {α : Type u} {β : Type v} {f : α → β} {l : filter β} {u : set β} :
u l(∀ (y : β), y u(∃ (x : α), f x = y))filter.map f (filter.comap f l) = l

theorem filter.le_map_comap_of_surjective {α : Type u} {β : Type v} {f : α → β} (hf : function.surjective f) (l : filter β) :

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.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 : α → β} :
(∀ (t : set β), t f(∃ (a : α), m a t))(filter.comap m f).ne_bot

theorem filter.ne_bot.comap_of_range_mem {α : Type u} {β : Type v} {f : filter β} {m : α → β} :
f.ne_botset.range m f(filter.comap m 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 α} :
m '' s f(filter.comap m f 𝓟 s).ne_bot

theorem filter.ne_bot.comap_of_surj {α : Type u} {β : Type v} {f : filter β} {m : α → β} :

theorem filter.ne_bot.comap_of_image_mem {α : Type u} {β : Type v} {f : filter β} {m : α → β} (hf : f.ne_bot) {s : set α} :
m '' s f(filter.comap m f).ne_bot

@[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} :
directed_on (f ⁻¹'o ge) {x : ι | p x}(∃ (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 α} :
t ft g(∀ (x : α), x t∀ (y : α), y tm x = m yx = y)filter.map m (f g) = filter.map m f filter.map m g

theorem filter.map_inf {α : Type u} {β : Type v} {f g : filter α} {m : α → β} :

theorem filter.map_eq_comap_of_inverse {α : Type u} {β : Type v} {f : filter α} {m : α → β} {n : β → α} :
m n = idn m = idfilter.map m f = filter.comap n f

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 β} :
(∀ (s : set α), s fm '' s g)g filter.map m f

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_sets {α : 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_sets_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_sets_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_sets {α : Type u} {β : Type v} {f : filter (α → β)} {g : filter α} {s : set (α → β)} {t : set α} :
s ft gs.seq t f.seq g

theorem filter.le_seq {α : Type u} {β : Type v} {f : filter (α → β)} {g : filter α} {h : filter β} :
(∀ (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 α} :
f₁ f₂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

@[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_sets' {α : Type u} {β : Type v} {s : set β} {f : filter α} {m : α → filter β} :
s f.bind m {a : α | s m a} f

@[simp]
theorem filter.mem_bind_sets {α : 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 β} :
(∀ᶠ (x : α) in f, g x l)f.bind g l

theorem filter.bind_mono {α : Type u} {β : Type v} {f₁ f₂ : filter α} {g₁ g₂ : α → filter β} :
f₁ f₂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_sets {α' β' γ' : 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_sets_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} :
(α → β)filter α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} :
filter.tendsto f l₁ l₂(∀ᶠ (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} :
filter.tendsto f l₁ l₂(∃ᶠ (x : α) in l₁, p (f x))(∃ᶠ (y : β) in l₂, p 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.tendsto_of_not_nonempty {α : Type u} {β : Type v} {f : α → β} {la : filter α} {lb : filter β} :
¬nonempty αfilter.tendsto f la lb

theorem filter.eventually_eq_of_left_inv_of_right_inv {α : Type u} {β : Type v} {f : α → β} {g₁ g₂ : β → α} {fa : filter α} {fb : filter β} :
(∀ᶠ (x : α) in fa, g₁ (f x) = x)(∀ᶠ (y : β) in fb, f (g₂ y) = y)filter.tendsto g₂ fb fag₁ =ᶠ[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 β} :
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 β} :
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 β} :
(∀ (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 β} :
(∀ (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 γ} :
filter.tendsto g y zfilter.tendsto f x yfilter.tendsto (g f) x z

theorem filter.tendsto.mono_left {α : Type u} {β : Type v} {f : α → β} {x y : filter α} {z : filter β} :
filter.tendsto f x zy xfilter.tendsto f y z

theorem filter.tendsto.mono_right {α : Type u} {β : Type v} {f : α → β} {x : filter α} {y z : filter β} :
filter.tendsto f x yy zfilter.tendsto f x 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 γ} :

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 β} :

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 : γ → α} :

theorem filter.comap_eq_of_inverse {α : Type u} {β : Type v} {f : filter α} {g : filter β} {φ : α → β} (ψ : β → α) :
ψ φ = idfilter.tendsto φ f gfilter.tendsto ψ g ffilter.comap φ g = f

theorem filter.map_eq_of_inverse {α : Type u} {β : Type v} {f : filter α} {g : filter β} {φ : α → β} (ψ : β → α) :
φ ψ = idfilter.tendsto φ f gfilter.tendsto ψ g ffilter.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 β} :
filter.tendsto f x₁ yfilter.tendsto f (x₁ x₂) y

theorem filter.tendsto_inf_right {α : Type u} {β : Type v} {f : α → β} {x₁ x₂ : filter α} {y : filter β} :
filter.tendsto f x₂ yfilter.tendsto f (x₁ x₂) y

theorem filter.tendsto.inf {α : Type u} {β : Type v} {f : α → β} {x₁ x₂ : filter α} {y₁ y₂ : filter β} :
filter.tendsto f x₁ y₁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 : ι) :
filter.tendsto f (x i) yfilter.tendsto f (⨅ (i : ι), x i) y

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_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

theorem filter.tendsto.not_tendsto {α : Type u} {β : Type v} {f : α → β} {a : filter α} {b₁ b₂ : filter β} (hf : filter.tendsto f a b₁) [a.ne_bot] :
disjoint b₁ b₂¬filter.tendsto f a 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} [decidable_pred p] :
filter.tendsto f (l₁ 𝓟 p) l₂filter.tendsto g (l₁ 𝓟 {x : α | ¬p x}) l₂filter.tendsto (λ (x : α), ite (p x) (f x) (g x)) l₁ l₂

Products of filters

def filter.prod {α : Type u} {β : Type v} :
filter αfilter βfilter × β)

Product of filters. This is the filter generated by cartesian products of elements of the component filters.

Equations
theorem filter.prod_mem_prod {α : Type u} {β : Type v} {s : set α} {t : set β} {f : filter α} {g : filter β} :
s ft gs.prod t f ×ᶠ g

theorem filter.mem_prod_iff {α : Type u} {β : Type v} {s : set × β)} {f : filter α} {g : filter β} :
s f ×ᶠ g ∃ (t₁ : set α) (H : t₁ f) (t₂ : set β) (H : t₂ g), t₁.prod t₂ s

theorem filter.comap_prod {α : Type u} {β : Type v} {γ : Type w} (f : α → β × γ) (b : filter β) (c : filter γ) :

theorem filter.eventually_prod_iff {α : Type u} {β : Type v} {p : α × β → Prop} {f : filter α} {g : filter β} :
(∀ᶠ (x : α × β) in f ×ᶠ g, p x) ∃ (pa : α → Prop) (ha : ∀ᶠ (x : α) in f, pa x) (pb : β → Prop) (hb : ∀ᶠ (y : β) in g, pb y), ∀ {x : α}, pa x∀ {y : β}, pb yp (x, y)

theorem filter.tendsto_fst {α : Type u} {β : Type v} {f : filter α} {g : filter β} :

theorem filter.tendsto_snd {α : Type u} {β : Type v} {f : filter α} {g : filter β} :

theorem filter.tendsto.prod_mk {α : Type u} {β : Type v} {γ : Type w} {f : filter α} {g : filter β} {h : filter γ} {m₁ : α → β} {m₂ : α → γ} :
filter.tendsto m₁ f gfilter.tendsto m₂ f hfilter.tendsto (λ (x : α), (m₁ x, m₂ x)) f (g ×ᶠ h)

theorem filter.eventually.prod_inl {α : Type u} {β : Type v} {la : filter α} {p : α → Prop} (h : ∀ᶠ (x : α) in la, p x) (lb : filter β) :
∀ᶠ (x : α × β) in la ×ᶠ lb, p x.fst

theorem filter.eventually.prod_inr {α : Type u} {β : Type v} {lb : filter β} {p : β → Prop} (h : ∀ᶠ (x : β) in lb, p x) (la : filter α) :
∀ᶠ (x : α × β) in la ×ᶠ lb, p x.snd

theorem filter.eventually.prod_mk {α : Type u} {β : Type v} {la : filter α} {pa : α → Prop} (ha : ∀ᶠ (x : α) in la, pa x) {lb : filter β} {pb : β → Prop} :
(∀ᶠ (y : β) in lb, pb y)(∀ᶠ (p : α × β) in la ×ᶠ lb, pa p.fst pb p.snd)

theorem filter.eventually.curry {α : Type u} {β : Type v} {la : filter α} {lb : filter β} {p : α × β → Prop} :
(∀ᶠ (x : α × β) in la ×ᶠ lb, p x)(∀ᶠ (x : α) in la, ∀ᶠ (y : β) in lb, p (x, y))

theorem filter.prod_infi_left {α : Type u} {β : Type v} {ι : Sort x} [nonempty ι] {f : ι → filter α} {g : filter β} :
(⨅ (i : ι), f i) ×ᶠ g = ⨅ (i : ι), f i ×ᶠ g

theorem filter.prod_infi_right {α : Type u} {β : Type v} {ι : Sort x} [nonempty ι] {f : filter α} {g : ι → filter β} :
(f ×ᶠ ⨅ (i : ι), g i) = ⨅ (i : ι), f ×ᶠ g i

theorem filter.prod_mono {α : Type u} {β : Type v} {f₁ f₂ : filter α} {g₁ g₂ : filter β} :
f₁ f₂g₁ g₂f₁ ×ᶠ g₁ f₂ ×ᶠ g₂

theorem filter.prod_comap_comap_eq {α₁ : Type u} {α₂ : Type v} {β₁ : Type w} {β₂ : Type x} {f₁ : filter α₁} {f₂ : filter α₂} {m₁ : β₁ → α₁} {m₂ : β₂ → α₂} :
filter.comap m₁ f₁ ×ᶠ filter.comap m₂ f₂ = filter.comap (λ (p : β₁ × β₂), (m₁ p.fst, m₂ p.snd)) (f₁ ×ᶠ f₂)

theorem filter.prod_comm' {α : Type u} {β : Type v} {f : filter α} {g : filter β} :

theorem filter.prod_comm {α : Type u} {β : Type v} {f : filter α} {g : filter β} :
f ×ᶠ g = filter.map (λ (p : β × α), (p.snd, p.fst)) (g ×ᶠ f)

theorem filter.prod_map_map_eq {α₁ : Type u} {α₂ : Type v} {β₁ : Type w} {β₂ : Type x} {f₁ : filter α₁} {f₂ : filter α₂} {m₁ : α₁ → β₁} {m₂ : α₂ → β₂} :
filter.map m₁ f₁ ×ᶠ filter.map m₂ f₂ = filter.map (λ (p : α₁ × α₂), (m₁ p.fst, m₂ p.snd)) (f₁ ×ᶠ f₂)

theorem filter.tendsto.prod_map {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} {f : α → γ} {g : β → δ} {a : filter α} {b : filter β} {c : filter γ} {d : filter δ} :
filter.tendsto f a cfilter.tendsto g b dfilter.tendsto (prod.map f g) (a ×ᶠ b) (c ×ᶠ d)

theorem filter.map_prod {α : Type u} {β : Type v} {γ : Type w} (m : α × β → γ) (f : filter α) (g : filter β) :
filter.map m (f ×ᶠ g) = (filter.map (λ (a : α) (b : β), m (a, b)) f).seq g

theorem filter.prod_eq {α : Type u} {β : Type v} {f : filter α} {g : filter β} :

theorem filter.prod_inf_prod {α : Type u} {β : Type v} {f₁ f₂ : filter α} {g₁ g₂ : filter β} :
(f₁ ×ᶠ g₁) (f₂ ×ᶠ g₂) = f₁ f₂ ×ᶠ g₁ g₂

@[simp]
theorem filter.prod_bot {α : Type u} {β : Type v} {f : filter α} :

@[simp]
theorem filter.bot_prod {α : Type u} {β : Type v} {g : filter β} :

@[simp]
theorem filter.prod_principal_principal {α : Type u} {β : Type v} {s : set α} {t : set β} :
𝓟 s ×ᶠ 𝓟 t = 𝓟 (s.prod t)

@[simp]
theorem filter.prod_pure_pure {α : Type u} {β : Type v} {a : α} {b : β} :
pure a ×ᶠ pure b = pure (a, b)

theorem filter.prod_eq_bot {α : Type u} {β : Type v} {f : filter α} {g : filter β} :
f ×ᶠ g = f = g =

theorem filter.prod_ne_bot {α : Type u} {β : Type v} {f : filter α} {g : filter β} :

theorem filter.ne_bot.prod {α : Type u} {β : Type v} {f : filter α} {g : filter β} :
f.ne_botg.ne_bot(f ×ᶠ g).ne_bot

@[instance]
def filter.prod_ne_bot' {α : Type u} {β : Type v} {f : filter α} {g : filter β} [hf : f.ne_bot] [hg : g.ne_bot] :

theorem filter.tendsto_prod_iff {α : Type u} {β : Type v} {γ : Type w} {f : α × β → γ} {x : filter α} {y : filter β} {z : filter γ} :
filter.tendsto f (x ×ᶠ y) z ∀ (W : set γ), W z(∃ (U : set α) (H : U x) (V : set β) (H : V y), ∀ (x : α) (y : β), x Uy Vf (x, y) W)

theorem set.eq_on.eventually_eq {α : Type u_1} {β : Type u_2} {s : set α} {f g : α → β} :
set.eq_on f g sf =ᶠ[𝓟 s] g