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.

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

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

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

Equations
source
@[protected, simp]
theorem filter.mem_mk {α : Type u} {s : set α} {t : set (set α)} {h₁ : set.univ ∈ t} {h₂ : ∀ {x y : set α}, x ∈ t → x ⊆ y → y ∈ t} {h₃ : ∀ {x y : set α}, x ∈ t → y ∈ t → x ∩ y ∈ t} :
s ∈ {sets := t, univ_sets := h₁, sets_of_superset := h₂, inter_sets := h₃} ↔ s ∈ t
source
@[protected, simp]
theorem filter.mem_sets {α : Type u} {f : filter α} {s : set α} :
s ∈ f.sets ↔ s ∈ f
source
@[protected, instance]
def filter.inhabited_mem {α : Type u} {f : filter α} :
inhabited {s // s ∈ f}
Equations
source
theorem filter.filter_eq {α : Type u} {f g : filter α} :
f.sets = g.sets → f = g
source
theorem filter.filter_eq_iff {α : Type u} {f g : filter α} :
f = g ↔ f.sets = g.sets
source
@[protected]
theorem filter.ext_iff {α : Type u} {f g : filter α} :
f = g ↔ ∀ (s : set α), s ∈ f ↔ s ∈ g
source
@[protected, ext]
theorem filter.ext {α : Type u} {f g : filter α} :
(∀ (s : set α), s ∈ f ↔ s ∈ g) → f = g
source
@[simp]
theorem filter.univ_mem {α : Type u} {f : filter α} :
set.univ ∈ f
source
theorem filter.mem_of_superset {α : Type u} {f : filter α} {x y : set α} (hx : x ∈ f) (hxy : x ⊆ y) :
y ∈ f
source
theorem filter.inter_mem {α : Type u} {f : filter α} {s t : set α} (hs : s ∈ f) (ht : t ∈ f) :
s ∩ t ∈ f
source
@[simp]
theorem filter.inter_mem_iff {α : Type u} {f : filter α} {s t : set α} :
s ∩ t ∈ f ↔ s ∈ f ∧ t ∈ f
source
theorem filter.diff_mem {α : Type u} {f : filter α} {s t : set α} (hs : s ∈ f) (ht : tᶜ ∈ f) :
s \ t ∈ f
source
theorem filter.univ_mem' {α : Type u} {f : filter α} {s : set α} (h : ∀ (a : α), a ∈ s) :
s ∈ f
source
theorem filter.mp_mem {α : Type u} {f : filter α} {s t : set α} (hs : s ∈ f) (h : {x : α | x ∈ s → x ∈ t} ∈ f) :
t ∈ f
source
theorem filter.congr_sets {α : Type u} {f : filter α} {s t : set α} (h : {x : α | x ∈ s ↔ x ∈ t} ∈ f) :
s ∈ f ↔ t ∈ f
source
@[simp]
theorem filter.bInter_mem {α : Type u} {f : filter α} {β : Type v} {s : β → set α} {is : set β} (hf : is.finite) :
(⋂ (i : β) (H : i ∈ is), s i) ∈ f ↔ ∀ (i : β), i ∈ is → s i ∈ f
source
@[simp]
theorem filter.bInter_finset_mem {α : Type u} {f : filter α} {β : Type v} {s : β → set α} (is : finset β) :
(⋂ (i : β) (H : i ∈ is), s i) ∈ f ↔ ∀ (i : β), i ∈ is → s i ∈ f
source
@[protected]
theorem finset.Inter_mem_sets {α : Type u} {f : filter α} {β : Type v} {s : β → set α} (is : finset β) :
(⋂ (i : β) (H : i ∈ is), s i) ∈ f ↔ ∀ (i : β), i ∈ is → s i ∈ f

Alias of bInter_finset_mem.

source
@[simp]
theorem filter.sInter_mem {α : Type u} {f : filter α} {s : set (set α)} (hfin : s.finite) :
⋂₀ s ∈ f ↔ ∀ (U : set α), U ∈ s → U ∈ f
source
@[simp]
theorem filter.Inter_mem {α : Type u} {f : filter α} {β : Type v} {s : β → set α} [fintype β] :
(⋂ (i : β), s i) ∈ f ↔ ∀ (i : β), s i ∈ f
source
theorem filter.exists_mem_subset_iff {α : Type u} {f : filter α} {s : set α} :
(∃ (t : set α) (H : t ∈ f), t ⊆ s) ↔ s ∈ f
source
theorem filter.monotone_mem {α : Type u} {f : filter α} :
monotone (λ (s : set α), s ∈ f)
source
theorem filter.exists_mem_and_iff {α : Type u} {f : filter α} {P Q : set α → Prop} (hP : antitone P) (hQ : antitone Q) :
((∃ (u : set α) (H : u ∈ f), P u) ∧ ∃ (u : set α) (H : u ∈ f), Q u) ↔ ∃ (u : set α) (H : u ∈ f), P u ∧ Q u
source
theorem filter.forall_in_swap {α : Type u} {f : filter α} {β : Type u_1} {p : set α → β → Prop} :
(∀ (a : set α), a ∈ f → ∀ (b : β), p a b) ↔ ∀ (b : β) (a : set α), a ∈ f → p a b
source
meta def tactic.interactive.filter_upwards (s : interactive.parse interactive.types.pexpr_list?) (wth : interactive.parse interactive.types.with_ident_list?) (tgt : interactive.parse (lean.parser.tk "using" *> interactive.types.texpr)?) :
tactic unit

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

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

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

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

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

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

Equations
source
@[protected, instance]
def filter.inhabited {α : Type u} :
inhabited (filter α)
Equations
source
@[simp]
theorem filter.mem_principal {α : Type u} {s t : set α} :
s ∈ 𝓟 t ↔ t ⊆ s
source
theorem filter.mem_principal_self {α : Type u} (s : set α) :
s ∈ 𝓟 s
source
def filter.join {α : Type u} (f : filter (filter α)) :
filter α

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

Equations
source
@[simp]
theorem filter.mem_join {α : Type u} {s : set α} {f : filter (filter α)} :
s ∈ f.join ↔ {t : filter α | s ∈ t} ∈ f
source
@[protected, instance]
def filter.partial_order {α : Type u} :
partial_order (filter α)
Equations
source
theorem filter.le_def {α : Type u} {f g : filter α} :
f ≤ g ↔ ∀ (x : set α), x ∈ g → x ∈ f
source
inductive filter.generate_sets {α : Type u} (g : set (set α)) :
set α → Prop

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

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

generate g is the largest filter containing the sets g.

Equations
source
theorem filter.sets_iff_generate {α : Type u} {s : set (set α)} {f : filter α} :
f ≤ filter.generate s ↔ s ⊆ f.sets
source
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
source
@[protected]
def filter.mk_of_closure {α : Type u} (s : set (set α)) (hs : (filter.generate s).sets = s) :
filter α

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

Galois insertion from sets of sets into filters.

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

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

Equations
source
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₂
source
theorem filter.mem_inf_of_left {α : Type u} {f g : filter α} {s : set α} (h : s ∈ f) :
s ∈ f ⊓ g
source
theorem filter.mem_inf_of_right {α : Type u} {f g : filter α} {s : set α} (h : s ∈ g) :
s ∈ f ⊓ g
source
theorem filter.inter_mem_inf {α : Type u} {f g : filter α} {s t : set α} (hs : s ∈ f) (ht : t ∈ g) :
s ∩ t ∈ f ⊓ g
source
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
source
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
source
@[protected, instance]
def filter.has_top {α : Type u} :
has_top (filter α)
Equations
source
theorem filter.mem_top_iff_forall {α : Type u} {s : set α} :
s ∈ ⊤ ↔ ∀ (x : α), x ∈ s
source
@[simp]
theorem filter.mem_top {α : Type u} {s : set α} :
s ∈ ⊤ ↔ s = set.univ
source
@[protected, instance]
def filter.complete_lattice {α : Type u} :
complete_lattice (filter α)
Equations
source
@[class]
structure filter.ne_bot {α : Type u} (f : filter α) :
Prop

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

Instances
source
theorem filter.ne_bot_iff {α : Type u} {f : filter α} :
f.ne_bot ↔ f ≠ ⊥
source
theorem filter.ne_bot.ne {α : Type u} {f : filter α} (hf : f.ne_bot) :
f ≠ ⊥
source
@[simp]
theorem filter.not_ne_bot {α : Type u_1} {f : filter α} :
¬f.ne_bot ↔ f = ⊥
source
theorem filter.ne_bot.mono {α : Type u} {f g : filter α} (hf : f.ne_bot) (hg : f ≤ g) :
g.ne_bot
source
theorem filter.ne_bot_of_le {α : Type u} {f g : filter α} [hf : f.ne_bot] (hg : f ≤ g) :
g.ne_bot
source
@[simp]
theorem filter.sup_ne_bot {α : Type u} {f g : filter α} :
(f ⊔ g).ne_bot ↔ f.ne_bot ∨ g.ne_bot
source
theorem filter.bot_sets_eq {α : Type u} :
⊥.sets = set.univ
source
theorem filter.sup_sets_eq {α : Type u} {f g : filter α} :
(f ⊔ g).sets = f.sets ∩ g.sets
source
theorem filter.Sup_sets_eq {α : Type u} {s : set (filter α)} :
(Sup s).sets = ⋂ (f : filter α) (H : f ∈ s), f.sets
source
theorem filter.supr_sets_eq {α : Type u} {ι : Sort x} {f : ι → filter α} :
(supr f).sets = ⋂ (i : ι), (f i).sets
source
theorem filter.generate_empty {α : Type u} :
filter.generate ∅ = ⊤
source
theorem filter.generate_univ {α : Type u} :
filter.generate set.univ = ⊥
source
theorem filter.generate_union {α : Type u} {s t : set (set α)} :
filter.generate (s ∪ t) = filter.generate s ⊓ filter.generate t
source
theorem filter.generate_Union {α : Type u} {ι : Sort x} {s : ι → set (set α)} :
filter.generate (⋃ (i : ι), s i) = ⨅ (i : ι), filter.generate (s i)
source
@[simp]
theorem filter.mem_bot {α : Type u} {s : set α} :
s ∈ ⊥
source
@[simp]
theorem filter.mem_sup {α : Type u} {f g : filter α} {s : set α} :
s ∈ f ⊔ g ↔ s ∈ f ∧ s ∈ g
source
theorem filter.union_mem_sup {α : Type u} {f g : filter α} {s t : set α} (hs : s ∈ f) (ht : t ∈ g) :
s ∪ t ∈ f ⊔ g
source
@[simp]
theorem filter.mem_Sup {α : Type u} {x : set α} {s : set (filter α)} :
x ∈ Sup s ↔ ∀ (f : filter α), f ∈ s → x ∈ f
source
@[simp]
theorem filter.mem_supr {α : Type u} {ι : Sort x} {x : set α} {f : ι → filter α} :
x ∈ supr f ↔ ∀ (i : ι), x ∈ f i
source
@[simp]
theorem filter.supr_ne_bot {α : Type u} {ι : Sort x} {f : ι → filter α} :
(⨆ (i : ι), f i).ne_bot ↔ ∃ (i : ι), (f i).ne_bot
source
theorem filter.infi_eq_generate {α : Type u} {ι : Sort x} (s : ι → filter α) :
infi s = filter.generate (⋃ (i : ι), (s i).sets)
source
theorem filter.mem_infi_of_mem {α : Type u} {ι : Sort x} {f : ι → filter α} (i : ι) {s : set α} :
s ∈ f i → (s ∈ ⨅ (i : ι), f i)
source
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
source
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
source
theorem filter.mem_infi' {α : Type u} {ι : Type u_1} {s : ι → filter α} {U : set α} :
(U ∈ ⨅ (i : ι), s i) ↔ ∃ (I : set ι), I.finite ∧ ∃ (V : ι → set α), (∀ (i : ι), V i ∈ s i) ∧ (∀ (i : ι), i ∉ I → V i = set.univ) ∧ (U = ⋂ (i : ι) (H : i ∈ I), V i) ∧ U = ⋂ (i : ι), V i
source
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
source
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
source
@[simp]
theorem filter.le_principal_iff {α : Type u} {s : set α} {f : filter α} :
f ≤ 𝓟 s ↔ s ∈ f
source
theorem filter.principal_mono {α : Type u} {s t : set α} :
𝓟 s ≤ 𝓟 t ↔ s ⊆ t
source
theorem filter.monotone_principal {α : Type u} :
monotone 𝓟
source
@[simp]
theorem filter.principal_eq_iff_eq {α : Type u} {s t : set α} :
𝓟 s = 𝓟 t ↔ s = t
source
@[simp]
theorem filter.join_principal_eq_Sup {α : Type u} {s : set (filter α)} :
(𝓟 s).join = Sup s
source
@[simp]
theorem filter.principal_univ {α : Type u} :
𝓟 set.univ = ⊤
source
@[simp]
theorem filter.principal_empty {α : Type u} :
𝓟 ∅ = ⊥
source
theorem filter.generate_eq_binfi {α : Type u} (S : set (set α)) :
filter.generate S = ⨅ (s : set α) (H : s ∈ S), 𝓟 s

Lattice equations #

source
theorem filter.empty_mem_iff_bot {α : Type u} {f : filter α} :
∅ ∈ f ↔ f = ⊥
source
theorem filter.nonempty_of_mem {α : Type u} {f : filter α} [hf : f.ne_bot] {s : set α} (hs : s ∈ f) :
s.nonempty
source
theorem filter.ne_bot.nonempty_of_mem {α : Type u} {f : filter α} (hf : f.ne_bot) {s : set α} (hs : s ∈ f) :
s.nonempty
source
@[simp]
theorem filter.empty_not_mem {α : Type u} (f : filter α) [f.ne_bot] :
∅ ∉ f
source
theorem filter.nonempty_of_ne_bot {α : Type u} (f : filter α) [f.ne_bot] :
nonempty α
source
theorem filter.compl_not_mem {α : Type u} {f : filter α} {s : set α} [f.ne_bot] (h : s ∈ f) :
sᶜ ∉ f
source
theorem filter.filter_eq_bot_of_is_empty {α : Type u} [is_empty α] (f : filter α) :
f = ⊥
source
@[protected]
theorem filter.disjoint_iff {α : Type u} {f g : filter α} :
disjoint f g ↔ ∃ (s : set α) (H : s ∈ f) (t : set α) (H : t ∈ g), disjoint s t
source
theorem filter.disjoint_of_disjoint_of_mem {α : Type u} {f g : filter α} {s t : set α} (h : disjoint s t) (hs : s ∈ f) (ht : t ∈ g) :
disjoint f g
source
theorem filter.inf_eq_bot_iff {α : Type u} {f g : filter α} :
f ⊓ g = ⊥ ↔ ∃ (U : set α) (H : U ∈ f) (V : set α) (H : V ∈ g), U ∩ V = ∅
source
@[protected]
def filter.unique {α : Type u} [is_empty α] :
unique (filter α)

There is exactly one filter on an empty type. -

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

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

source
theorem filter.forall_mem_nonempty_iff_ne_bot {α : Type u} {f : filter α} :
(∀ (s : set α), s ∈ f → s.nonempty) ↔ f.ne_bot
source
theorem filter.nontrivial_iff_nonempty {α : Type u} :
nontrivial (filter α) ↔ nonempty α
source
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
source
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
source
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
source
theorem filter.infi_sets_eq {α : Type u} {ι : Sort x} {f : ι → filter α} (h : directed ge f) [ne : nonempty ι] :
(infi f).sets = ⋃ (i : ι), (f i).sets
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
@[simp]
theorem filter.sup_join {α : Type u} {f₁ f₂ : filter (filter α)} :
f₁.join ⊔ f₂.join = (f₁ ⊔ f₂).join
source
@[simp]
theorem filter.supr_join {α : Type u} {ι : Sort w} {f : ι → filter (filter α)} :
(⨆ (x : ι), (f x).join) = (⨆ (x : ι), f x).join
source
@[protected, instance]
def filter.distrib_lattice {α : Type u} :
distrib_lattice (filter α)
Equations
source
@[protected, instance]
def filter.order.coframe {α : Type u} :
order.coframe (filter α)
Equations
source
theorem filter.mem_infi_finset {α : Type u} {β : Type v} {s : finset α} {f : α → filter β} {t : set β} :
(t ∈ ⨅ (a : α) (H : a ∈ s), f a) ↔ ∃ (p : α → set β), (∀ (a : α), a ∈ s → p a ∈ f a) ∧ t = ⋂ (a : α) (H : a ∈ s), p a
source
theorem filter.infi_ne_bot_of_directed' {α : Type u} {ι : Sort x} {f : ι → filter α} [nonempty ι] (hd : directed ge f) (hb : ∀ (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 ι.

source
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) :
(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 α.

source
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
source
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
source
theorem filter.infi_sets_induct {α : Type u} {ι : Sort x} {f : ι → filter α} {s : set α} (hs : s ∈ infi f) {p : set α → Prop} (uni : p set.univ) (ins : ∀ {i : ι} {s₁ s₂ : set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)) :
p s

principal equations #

source
@[simp]
theorem filter.inf_principal {α : Type u} {s t : set α} :
𝓟 s ⊓ 𝓟 t = 𝓟 (s ∩ t)
source
@[simp]
theorem filter.sup_principal {α : Type u} {s t : set α} :
𝓟 s ⊔ 𝓟 t = 𝓟 (s ∪ t)
source
@[simp]
theorem filter.supr_principal {α : Type u} {ι : Sort w} {s : ι → set α} :
(⨆ (x : ι), 𝓟 (s x)) = 𝓟 (⋃ (i : ι), s i)
source
@[simp]
theorem filter.principal_eq_bot_iff {α : Type u} {s : set α} :
𝓟 s = ⊥ ↔ s = ∅
source
@[simp]
theorem filter.principal_ne_bot_iff {α : Type u} {s : set α} :
(𝓟 s).ne_bot ↔ s.nonempty
source
theorem filter.is_compl_principal {α : Type u} (s : set α) :
is_compl (𝓟 s) (𝓟 sᶜ)
source
theorem filter.mem_inf_principal' {α : Type u} {f : filter α} {s t : set α} :
s ∈ f ⊓ 𝓟 t ↔ tᶜ ∪ s ∈ f
source
theorem filter.mem_inf_principal {α : Type u} {f : filter α} {s t : set α} :
s ∈ f ⊓ 𝓟 t ↔ {x : α | x ∈ t → x ∈ s} ∈ f
source
theorem filter.supr_inf_principal {α : Type u} {ι : Sort x} (f : ι → filter α) (s : set α) :
(⨆ (i : ι), f i ⊓ 𝓟 s) = (⨆ (i : ι), f i) ⊓ 𝓟 s
source
theorem filter.inf_principal_eq_bot {α : Type u} {f : filter α} {s : set α} :
f ⊓ 𝓟 s = ⊥ ↔ sᶜ ∈ f
source
theorem filter.mem_of_eq_bot {α : Type u} {f : filter α} {s : set α} (h : f ⊓ 𝓟 sᶜ = ⊥) :
s ∈ f
source
theorem filter.diff_mem_inf_principal_compl {α : Type u} {f : filter α} {s : set α} (hs : s ∈ f) (t : set α) :
s \ t ∈ f ⊓ 𝓟 tᶜ
source
theorem filter.principal_le_iff {α : Type u} {s : set α} {f : filter α} :
𝓟 s ≤ f ↔ ∀ (V : set α), V ∈ f → s ⊆ V
source
@[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)
source
@[simp]
theorem filter.infi_principal_fintype {α : Type u} {ι : Type w} [fintype ι] (f : ι → set α) :
(⨅ (i : ι), 𝓟 (f i)) = 𝓟 (⋂ (i : ι), f i)
source
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)
source
theorem filter.join_mono {α : Type u} {f₁ f₂ : filter (filter α)} (h : f₁ ≤ f₂) :
f₁.join ≤ f₂.join

Eventually #

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

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

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

Alias of eventually_all_finite.

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

Alias of eventually_all_finset.

source
@[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
source
@[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
source
@[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)
source
@[simp]
theorem filter.eventually_bot {α : Type u} {p : α → Prop} :
∀ᶠ (x : α) in ⊥, p x
source
@[simp]
theorem filter.eventually_top {α : Type u} {p : α → Prop} :
(∀ᶠ (x : α) in ⊤, p x) ↔ ∀ (x : α), p x
source
@[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
source
@[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)
source
@[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
source
@[simp]
theorem filter.eventually_principal {α : Type u} {a : set α} {p : α → Prop} :
(∀ᶠ (x : α) in 𝓟 a, p x) ↔ ∀ (x : α), x ∈ a → p x
source
theorem filter.eventually_inf {α : Type u} {f g : filter α} {p : α → Prop} :
(∀ᶠ (x : α) in f ⊓ g, p x) ↔ ∃ (s : set α) (H : s ∈ f) (t : set α) (H : t ∈ g), ∀ (x : α), x ∈ s ∩ t → p x
source
theorem filter.eventually_inf_principal {α : Type u} {f : filter α} {p : α → Prop} {s : set α} :
(∀ᶠ (x : α) in f ⊓ 𝓟 s, p x) ↔ ∀ᶠ (x : α) in f, x ∈ s → p x

Frequently #

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

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

Equations
source
theorem filter.eventually.frequently {α : Type u} {f : filter α} [f.ne_bot] {p : α → Prop} (h : ∀ᶠ (x : α) in f, p x) :
∃ᶠ (x : α) in f, p x
source
theorem filter.frequently_of_forall {α : Type u} {f : filter α} [f.ne_bot] {p : α → Prop} (h : ∀ (x : α), p x) :
∃ᶠ (x : α) in f, p x
source
theorem filter.frequently.mp {α : Type u} {p q : α → Prop} {f : filter α} (h : ∃ᶠ (x : α) in f, p x) (hpq : ∀ᶠ (x : α) in f, p x → q x) :
∃ᶠ (x : α) in f, q x
source
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
source
theorem filter.frequently.mono {α : Type u} {p q : α → Prop} {f : filter α} (h : ∃ᶠ (x : α) in f, p x) (hpq : ∀ (x : α), p x → q x) :
∃ᶠ (x : α) in f, q x
source
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
source
theorem filter.eventually.and_frequently {α : Type u} {p q : α → Prop} {f : filter α} (hp : ∀ᶠ (x : α) in f, p x) (hq : ∃ᶠ (x : α) in f, q x) :
∃ᶠ (x : α) in f, p x ∧ q x
source
theorem filter.frequently.exists {α : Type u} {p : α → Prop} {f : filter α} (hp : ∃ᶠ (x : α) in f, p x) :
∃ (x : α), p x
source
theorem filter.eventually.exists {α : Type u} {p : α → Prop} {f : filter α} [f.ne_bot] (hp : ∀ᶠ (x : α) in f, p x) :
∃ (x : α), p x
source
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)
source
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)
source
@[simp]
theorem filter.not_eventually {α : Type u} {p : α → Prop} {f : filter α} :
(¬∀ᶠ (x : α) in f, p x) ↔ ∃ᶠ (x : α) in f, ¬p x
source
@[simp]
theorem filter.not_frequently {α : Type u} {p : α → Prop} {f : filter α} :
(¬∃ᶠ (x : α) in f, p x) ↔ ∀ᶠ (x : α) in f, ¬p x
source
@[simp]
theorem filter.frequently_true_iff_ne_bot {α : Type u} (f : filter α) :
(∃ᶠ (x : α) in f, true) ↔ f.ne_bot
source
@[simp]
theorem filter.frequently_false {α : Type u} (f : filter α) :
¬∃ᶠ (x : α) in f, false
source
@[simp]
theorem filter.frequently_const {α : Type u} {f : filter α} [f.ne_bot] {p : Prop} :
(∃ᶠ (x : α) in f, p) ↔ p
source
@[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
source
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
source
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
source
@[simp]
theorem filter.frequently_imp_distrib {α : Type u} {f : filter α} {p q : α → Prop} :
(∃ᶠ (x : α) in f, p x → q x) ↔ (∀ᶠ (x : α) in f, p x) → (∃ᶠ (x : α) in f, q x)
source
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)
source
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
source
@[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
source
@[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
source
@[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
source
@[simp]
theorem filter.frequently_bot {α : Type u} {p : α → Prop} :
¬∃ᶠ (x : α) in ⊥, p x
source
@[simp]
theorem filter.frequently_top {α : Type u} {p : α → Prop} :
(∃ᶠ (x : α) in ⊤, p x) ↔ ∃ (x : α), p x
source
@[simp]
theorem filter.frequently_principal {α : Type u} {a : set α} {p : α → Prop} :
(∃ᶠ (x : α) in 𝓟 a, p x) ↔ ∃ (x : α) (H : x ∈ a), p x
source
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
source
@[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
source
@[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” #

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

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

source
@[simp]
theorem filter.eventually_eq_univ {α : Type u} {s : set α} {l : filter α} :
s =ᶠ[l] set.univ ↔ s ∈ l
source
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
source
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
source
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
source
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
source
theorem filter.eventually_eq.refl {α : Type u} {β : Type v} (l : filter α) (f : α → β) :
f =ᶠ[l] f
source
theorem filter.eventually_eq.rfl {α : Type u} {β : Type v} {l : filter α} {f : α → β} :
f =ᶠ[l] f
source
theorem filter.eventually_eq.symm {α : Type u} {β : Type v} {f g : α → β} {l : filter α} (H : f =ᶠ[l] g) :
g =ᶠ[l] f
source
theorem filter.eventually_eq.trans {α : Type u} {β : Type v} {l : filter α} {f g h : α → β} (H₁ : f =ᶠ[l] g) (H₂ : g =ᶠ[l] h) :
f =ᶠ[l] h
source
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)
source
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
source
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)
source
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
source
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
source
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
source
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)⁻¹
source
theorem filter.eventually_eq.sub {α : Type u} {β : Type v} [has_sub β] {f f' g g' : α → β} {l : filter α} (h : f =ᶠ[l] g) (h' : f' =ᶠ[l] g') :
(λ (x : α), f x - f' x) =ᶠ[l] λ (x : α), g x - g' x
source
theorem filter.eventually_eq.div {α : Type u} {β : Type v} [has_div β] {f f' g g' : α → β} {l : filter α} (h : f =ᶠ[l] g) (h' : f' =ᶠ[l] g') :
(λ (x : α), f x / f' x) =ᶠ[l] λ (x : α), g x / g' x
source
theorem filter.eventually_eq.const_vadd {α : Type u} {β : Type v} {𝕜 : Type u_1} [has_vadd 𝕜 β] {l : filter α} {f g : α → β} (h : f =ᶠ[l] g) (c : 𝕜) :
(λ (x : α), c +ᵥ f x) =ᶠ[l] λ (x : α), c +ᵥ g x
source
theorem filter.eventually_eq.const_smul {α : Type u} {β : Type v} {𝕜 : Type u_1} [has_scalar 𝕜 β] {l : filter α} {f g : α → β} (h : f =ᶠ[l] g) (c : 𝕜) :
(λ (x : α), c • f x) =ᶠ[l] λ (x : α), c • g x
source
theorem filter.eventually_eq.vadd {α : Type u} {β : Type v} {𝕜 : Type u_1} [has_vadd 𝕜 β] {l : filter α} {f f' : α → 𝕜} {g g' : α → β} (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') :
(λ (x : α), f x +ᵥ g x) =ᶠ[l] λ (x : α), f' x +ᵥ g' x
source
theorem filter.eventually_eq.smul {α : Type u} {β : Type v} {𝕜 : Type u_1} [has_scalar 𝕜 β] {l : filter α} {f f' : α → 𝕜} {g g' : α → β} (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') :
(λ (x : α), f x • g x) =ᶠ[l] λ (x : α), f' x • g' x
source
theorem filter.eventually_eq.sup {α : Type u} {β : Type v} [has_sup β] {l : filter α} {f f' g g' : α → β} (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') :
(λ (x : α), f x ⊔ g x) =ᶠ[l] λ (x : α), f' x ⊔ g' x
source
theorem filter.eventually_eq.inf {α : Type u} {β : Type v} [has_inf β] {l : filter α} {f f' g g' : α → β} (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') :
(λ (x : α), f x ⊓ g x) =ᶠ[l] λ (x : α), f' x ⊓ g' x
source
theorem filter.eventually_eq.preimage {α : Type u} {β : Type v} {l : filter α} {f g : α → β} (h : f =ᶠ[l] g) (s : set β) :
f ⁻¹' s =ᶠ[l] g ⁻¹' s
source
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'
source
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'
source
theorem filter.eventually_eq.compl {α : Type u} {s t : set α} {l : filter α} (h : s =ᶠ[l] t) :
sᶜ =ᶠ[l] tᶜ
source
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'
source
theorem filter.eventually_eq_empty {α : Type u} {s : set α} {l : filter α} :
s =ᶠ[l] ∅ ↔ ∀ᶠ (x : α) in l, x ∉ s
source
theorem filter.inter_eventually_eq_left {α : Type u} {s t : set α} {l : filter α} :
s ∩ t =ᶠ[l] s ↔ ∀ᶠ (x : α) in l, x ∈ s → x ∈ t
source
theorem filter.inter_eventually_eq_right {α : Type u} {s t : set α} {l : filter α} :
s ∩ t =ᶠ[l] t ↔ ∀ᶠ (x : α) in l, x ∈ t → x ∈ s
source
@[simp]
theorem filter.eventually_eq_principal {α : Type u} {β : Type v} {s : set α} {f g : α → β} :
f =ᶠ[𝓟 s] g ↔ set.eq_on f g s
source
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 ∈ s → f x = g x
source
theorem filter.eventually_eq.sub_eq {α : Type u} {β : Type v} [add_group β] {f g : α → β} {l : filter α} (h : f =ᶠ[l] g) :
f - g =ᶠ[l] 0
source
theorem filter.eventually_eq_iff_sub {α : Type u} {β : Type v} [add_group β] {f g : α → β} {l : filter α} :
f =ᶠ[l] g ↔ f - g =ᶠ[l] 0
source
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
source
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'
source
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'
source
theorem filter.eventually_eq.le {α : Type u} {β : Type v} [preorder β] {l : filter α} {f g : α → β} (h : f =ᶠ[l] g) :
f ≤ᶠ[l] g
source
theorem filter.eventually_le.refl {α : Type u} {β : Type v} [preorder β] (l : filter α) (f : α → β) :
f ≤ᶠ[l] f
source
theorem filter.eventually_le.rfl {α : Type u} {β : Type v} [preorder β] {l : filter α} {f : α → β} :
f ≤ᶠ[l] f
source
theorem filter.eventually_le.trans {α : Type u} {β : Type v} [preorder β] {l : filter α} {f g h : α → β} (H₁ : f ≤ᶠ[l] g) (H₂ : g ≤ᶠ[l] h) :
f ≤ᶠ[l] h
source
theorem filter.eventually_eq.trans_le {α : Type u} {β : Type v} [preorder β] {l : filter α} {f g h : α → β} (H₁ : f =ᶠ[l] g) (H₂ : g ≤ᶠ[l] h) :
f ≤ᶠ[l] h
source
theorem filter.eventually_le.trans_eq {α : Type u} {β : Type v} [preorder β] {l : filter α} {f g h : α → β} (H₁ : f ≤ᶠ[l] g) (H₂ : g =ᶠ[l] h) :
f ≤ᶠ[l] h
source
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
source
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
source
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
source
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
source
theorem filter.eventually.ne_top_of_lt {α : Type u} {β : Type v} [partial_order β] [order_top β] {l : filter α} {f g : α → β} (h : ∀ᶠ (x : α) in l, f x < g x) :
∀ᶠ (x : α) in l, f x ≠ ⊤
source
theorem filter.eventually.lt_top_of_ne {α : Type u} {β : Type v} [partial_order β] [order_top β] {l : filter α} {f : α → β} (h : ∀ᶠ (x : α) in l, f x ≠ ⊤) :
∀ᶠ (x : α) in l, f x < ⊤
source
theorem filter.eventually.lt_top_iff_ne_top {α : Type u} {β : Type v} [partial_order β] [order_top β] {l : filter α} {f : α → β} :
(∀ᶠ (x : α) in l, f x < ⊤) ↔ ∀ᶠ (x : α) in l, f x ≠ ⊤
source
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'
source
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'
source
theorem filter.eventually_le.compl {α : Type u} {s t : set α} {l : filter α} (h : s ≤ᶠ[l] t) :
tᶜ ≤ᶠ[l] sᶜ
source
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'
source
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 #

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

The forward map of a filter

Equations
source
@[simp]
theorem filter.map_principal {α : Type u} {β : Type v} {s : set α} {f : α → β} :
filter.map f (𝓟 s) = 𝓟 (f '' s)
source
@[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)
source
@[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)
source
@[simp]
theorem filter.mem_map {α : Type u} {β : Type v} {f : filter α} {m : α → β} {t : set β} :
t ∈ filter.map m f ↔ m ⁻¹' t ∈ f
source
theorem filter.mem_map' {α : Type u} {β : Type v} {f : filter α} {m : α → β} {t : set β} :
t ∈ filter.map m f ↔ {x : α | m x ∈ t} ∈ f
source
theorem filter.image_mem_map {α : Type u} {β : Type v} {f : filter α} {m : α → β} {s : set α} (hs : s ∈ f) :
m '' s ∈ filter.map m f
source
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
source
theorem filter.range_mem_map {α : Type u} {β : Type v} {f : filter α} {m : α → β} :
set.range m ∈ filter.map m f
source
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
source
@[simp]
theorem filter.map_id {α : Type u} {f : filter α} :
filter.map id f = f
source
@[simp]
theorem filter.map_id' {α : Type u} {f : filter α} :
filter.map (λ (x : α), x) f = f
source
@[simp]
theorem filter.map_compose {α : Type u} {β : Type v} {γ : Type w} {m : α → β} {m' : β → γ} :
filter.map m' ∘ filter.map m = filter.map (m' ∘ m)
source
@[simp]
theorem filter.map_map {α : Type u} {β : Type v} {γ : Type w} {f : filter α} {m : α → β} {m' : β → γ} :
filter.map m' (filter.map m f) = filter.map (m' ∘ m) f
source
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.

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

The inverse map of a filter

Equations
source
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)
source
@[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 = b → P a
source
@[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
source
def filter.bind {α : Type u} {β : Type v} (f : filter α) (m : α → 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
source
def filter.seq {α : Type u} {β : Type v} (f : filter (α → β)) (g : filter α) :
filter β

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

Equations
source
@[protected, instance]
def filter.has_pure  :
has_pure filter

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
source
@[protected, instance]
def filter.has_bind  :
has_bind filter
Equations
source
@[protected, instance]
def filter.has_seq  :
has_seq filter
Equations
source
@[protected, instance]
def filter.functor  :
functor filter
Equations
source
theorem filter.pure_sets {α : Type u} (a : α) :
(pure a).sets = {s : set α | a ∈ s}
source
@[simp]
theorem filter.mem_pure {α : Type u} {a : α} {s : set α} :
s ∈ pure a ↔ a ∈ s
source
@[simp]
theorem filter.eventually_pure {α : Type u} {a : α} {p : α → Prop} :
(∀ᶠ (x : α) in pure a, p x) ↔ p a
source
@[simp]
theorem filter.principal_singleton {α : Type u} (a : α) :
𝓟 {a} = pure a
source
@[simp]
theorem filter.map_pure {α : Type u} {β : Type v} (f : α → β) (a : α) :
filter.map f (pure a) = pure (f a)
source
@[simp]
theorem filter.join_pure {α : Type u} (f : filter α) :
(pure f).join = f
source
@[simp]
theorem filter.pure_bind {α : Type u} {β : Type v} (a : α) (m : α → filter β) :
(pure a).bind m = m a
source
@[protected]
def filter.monad  :
monad filter

The monad structure on filters.

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

map and comap equations #

source
@[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
source
theorem filter.preimage_mem_comap {α : Type u} {β : Type v} {g : filter β} {m : α → β} {t : set β} (ht : t ∈ g) :
m ⁻¹' t ∈ filter.comap m g
source
theorem filter.comap_id {α : Type u} {f : filter α} :
filter.comap id f = f
source
theorem filter.comap_const_of_not_mem {α : Type u} {β : Type v} {g : filter β} {t : set β} {x : β} (ht : t ∈ g) (hx : x ∉ t) :
filter.comap (λ (y : α), x) g = ⊥
source
theorem filter.comap_const_of_mem {α : Type u} {β : Type v} {g : filter β} {x : β} (h : ∀ (t : set β), t ∈ g → x ∈ t) :
filter.comap (λ (y : α), x) g = ⊤
source
theorem filter.map_const {α : Type u} {β : Type v} {f : filter α} [f.ne_bot] {c : β} :
filter.map (λ (x : α), c) f = pure c
source
theorem filter.comap_comap {α : Type u} {β : Type v} {γ : Type w} {f : filter α} {m : γ → β} {n : β → α} :
filter.comap m (filter.comap n f) = filter.comap (n ∘ m) f

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

    φ
  α → β
θ ↓   ↓ ψ
  γ → δ
    ρ
source
theorem filter.map_comm {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} {φ : α → β} {θ : α → γ} {ψ : β → δ} {ρ : γ → δ} (H : ψ ∘ φ = ρ ∘ θ) (F : filter α) :
filter.map ψ (filter.map φ F) = filter.map ρ (filter.map θ F)
source
theorem filter.comap_comm {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} {φ : α → β} {θ : α → γ} {ψ : β → δ} {ρ : γ → δ} (H : ψ ∘ φ = ρ ∘ θ) (G : filter δ) :
filter.comap φ (filter.comap ψ G) = filter.comap θ (filter.comap ρ G)
source
@[simp]
theorem filter.comap_principal {α : Type u} {β : Type v} {m : α → β} {t : set β} :
filter.comap m (𝓟 t) = 𝓟 (m ⁻¹' t)
source
@[simp]
theorem filter.comap_pure {α : Type u} {β : Type v} {m : α → β} {b : β} :
filter.comap m (pure b) = 𝓟 (m ⁻¹' {b})
source
theorem filter.map_le_iff_le_comap {α : Type u} {β : Type v} {f : filter α} {g : filter β} {m : α → β} :
filter.map m f ≤ g ↔ f ≤ filter.comap m g
source
theorem filter.gc_map_comap {α : Type u} {β : Type v} (m : α → β) :
galois_connection (filter.map m) (filter.comap m)
source
theorem filter.map_mono {α : Type u} {β : Type v} {m : α → β} :
monotone (filter.map m)
source
theorem filter.comap_mono {α : Type u} {β : Type v} {m : α → β} :
monotone (filter.comap m)
source
@[simp]
theorem filter.map_bot {α : Type u} {β : Type v} {m : α → β} :
filter.map m ⊥ = ⊥
source
@[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₂
source
@[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)
source
@[simp]
theorem filter.comap_top {α : Type u} {β : Type v} {m : α → β} :
filter.comap m ⊤ = ⊤
source
@[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₂
source
@[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)
source
theorem filter.le_comap_top {α : Type u} {β : Type v} (f : α → β) (l : filter α) :
l ≤ filter.comap f ⊤
source
theorem filter.map_comap_le {α : Type u} {β : Type v} {g : filter β} {m : α → β} :
filter.map m (filter.comap m g) ≤ g
source
theorem filter.le_comap_map {α : Type u} {β : Type v} {f : filter α} {m : α → β} :
f ≤ filter.comap m (filter.map m f)
source
@[simp]
theorem filter.comap_bot {α : Type u} {β : Type v} {m : α → β} :
filter.comap m ⊥ = ⊥
source
theorem filter.disjoint_comap {α : Type u} {β : Type v} {g₁ g₂ : filter β} {m : α → β} (h : disjoint g₁ g₂) :
disjoint (filter.comap m g₁) (filter.comap m g₂)
source
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)
source
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
source
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₂
source
theorem filter.map_comap {α : Type u} {β : Type v} (f : filter β) (m : α → β) :
filter.map m (filter.comap m f) = f ⊓ 𝓟 (set.range m)
source
theorem filter.map_comap_of_mem {α : Type u} {β : Type v} {f : filter β} {m : α → β} (hf : set.range m ∈ f) :
filter.map m (filter.comap m f) = f
source
@[protected, instance]
def filter.can_lift {α : Type u} {β : Type v} [can_lift α β] :
can_lift (filter α) (filter β)
Equations
source
theorem filter.comap_le_comap_iff {α : Type u} {β : Type v} {f g : filter β} {m : α → β} (hf : set.range m ∈ f) :
filter.comap m f ≤ filter.comap m g ↔ f ≤ g
source
theorem filter.map_comap_of_surjective {α : Type u} {β : Type v} {f : α → β} (hf : function.surjective f) (l : filter β) :
filter.map f (filter.comap f l) = l
source
theorem function.surjective.filter_map_top {α : Type u} {β : Type v} {f : α → β} (hf : function.surjective f) :
filter.map f ⊤ = ⊤
source
theorem filter.subtype_coe_map_comap {α : Type u} (s : set α) (f : filter α) :
filter.map coe (filter.comap coe f) = f ⊓ 𝓟 s
source
theorem filter.subtype_coe_map_comap_prod {α : Type u} (s : set α) (f : filter (α × α)) :
filter.map coe (filter.comap coe f) = f ⊓ 𝓟 (s ×ˢ s)
source
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
source
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
source
theorem filter.comap_map {α : Type u} {β : Type v} {f : filter α} {m : α → β} (h : function.injective m) :
filter.comap m (filter.map m f) = f
source
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
source
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 ∈ s → m x = m y → x = y) (h : filter.map m f ≤ filter.map m g) :
f ≤ g
source
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 ∈ s → m x = m y → x = y) :
filter.map m f ≤ filter.map m g ↔ f ≤ g
source
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 ∈ s → m x = m y → x = y) (h : filter.map m f = filter.map m g) :
f = g
source
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
source
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)
source
theorem filter.comap_ne_bot {α : Type u} {β : Type v} {f : filter β} {m : α → β} (hm : ∀ (t : set β), t ∈ f → (∃ (a : α), m a ∈ t)) :
(filter.comap m f).ne_bot
source
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
source
theorem filter.comap_ne_bot_iff_compl_range {α : Type u} {β : Type v} {f : filter β} {m : α → β} :
(filter.comap m f).ne_bot ↔ (set.range m)ᶜ ∉ f
source
theorem filter.ne_bot.comap_of_range_mem {α : Type u} {β : Type v} {f : filter β} {m : α → β} (hf : f.ne_bot) (hm : set.range m ∈ f) :
(filter.comap m f).ne_bot
source
@[simp]
theorem filter.comap_fst_ne_bot_iff {α : Type u} {β : Type v} {f : filter α} :
(filter.comap prod.fst f).ne_bot ↔ f.ne_bot ∧ nonempty β
source
@[instance]
theorem filter.comap_fst_ne_bot {α : Type u} {β : Type v} [nonempty β] {f : filter α} [f.ne_bot] :
(filter.comap prod.fst f).ne_bot
source
@[simp]
theorem filter.comap_snd_ne_bot_iff {α : Type u} {β : Type v} {f : filter β} :
(filter.comap prod.snd f).ne_bot ↔ nonempty α ∧ f.ne_bot
source
@[instance]
theorem filter.comap_snd_ne_bot {α : Type u} {β : Type v} [nonempty α] {f : filter β} [f.ne_bot] :
(filter.comap prod.snd f).ne_bot
source
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
source
@[simp]
theorem filter.comap_eval_ne_bot_iff {ι : Type u_1} {α : ι → Type u_2} [∀ (j : ι), nonempty (α j)] {i : ι} {f : filter (α i)} :
(filter.comap (function.eval i) f).ne_bot ↔ f.ne_bot
source
@[instance]
theorem filter.comap_eval_ne_bot {ι : Type u_1} {α : ι → Type u_2} [∀ (j : ι), nonempty (α j)] (i : ι) (f : filter (α i)) [f.ne_bot] :
(filter.comap (function.eval i) f).ne_bot
source
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) :
(filter.comap m f ⊓ 𝓟 s).ne_bot
source
theorem filter.comap_coe_ne_bot_of_le_principal {γ : Type w} {s : set γ} {l : filter γ} [h : l.ne_bot] (h' : l ≤ 𝓟 s) :
(filter.comap coe l).ne_bot
source
theorem filter.ne_bot.comap_of_surj {α : Type u} {β : Type v} {f : filter β} {m : α → β} (hf : f.ne_bot) (hm : function.surjective m) :
(filter.comap m f).ne_bot
source
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) :
(filter.comap m f).ne_bot
source
@[simp]
theorem filter.map_eq_bot_iff {α : Type u} {β : Type v} {f : filter α} {m : α → β} :
filter.map m f = ⊥ ↔ f = ⊥
source
theorem filter.map_ne_bot_iff {α : Type u} {β : Type v} (f : α → β) {F : filter α} :
(filter.map f F).ne_bot ↔ F.ne_bot
source
theorem filter.ne_bot.map {α : Type u} {β : Type v} {f : filter α} (hf : f.ne_bot) (m : α → β) :
(filter.map m f).ne_bot
source
@[protected, instance]
def filter.map_ne_bot {α : Type u} {β : Type v} {f : filter α} {m : α → β} [hf : f.ne_bot] :
(filter.map m f).ne_bot
source
theorem filter.sInter_comap_sets {α : Type u} {β : Type v} (f : α → β) (F : filter β) :
⋂₀ (filter.comap f F).sets = ⋂ (U : set β) (H : U ∈ F), f ⁻¹' U
source
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)
source
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)
source
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)
source
theorem filter.map_inf_le {α : Type u} {β : Type v} {f g : filter α} {m : α → β} :
filter.map m (f ⊓ g) ≤ filter.map m f ⊓ filter.map m g
source
theorem filter.map_inf {α : Type u} {β : Type v} {f g : filter α} {m : α → β} (h : function.injective m) :
filter.map m (f ⊓ g) = filter.map m f ⊓ filter.map m g
source
theorem filter.map_inf' {α : Type u} {β : Type v} {f g : filter α} {m : α → β} {t : set α} (htf : t ∈ f) (htg : t ∈ g) (h : set.inj_on m t) :
filter.map m (f ⊓ g) = filter.map m f ⊓ filter.map m g
source
theorem filter.disjoint_map {α : Type u} {β : Type v} {m : α → β} (hm : function.injective m) {f₁ f₂ : filter α} :
disjoint (filter.map m f₁) (filter.map m f₂) ↔ disjoint f₁ f₂
source
theorem filter.map_eq_comap_of_inverse {α : Type u} {β : Type v} {f : filter α} {m : α → β} {n : β → α} (h₁ : m ∘ n = id) (h₂ : n ∘ m = id) :
filter.map m f = filter.comap n f
source
theorem filter.map_equiv_symm {α : Type u} {β : Type v} (e : α ≃ β) (f : filter β) :
filter.map ⇑(e.symm) f = filter.comap ⇑e f
source
theorem filter.comap_equiv_symm {α : Type u} {β : Type v} (e : α ≃ β) (f : filter α) :
filter.comap ⇑(e.symm) f = filter.map ⇑e f
source
theorem filter.map_swap_eq_comap_swap {α : Type u} {β : Type v} {f : filter (α × β)} :
prod.swap <$> f = filter.comap prod.swap f
source
theorem filter.le_map {α : Type u} {β : Type v} {f : filter α} {m : α → β} {g : filter β} (h : ∀ (s : set α), s ∈ f → m '' s ∈ g) :
g ≤ filter.map m f
source
@[protected]
theorem filter.push_pull {α : Type u} {β : Type v} (f : α → β) (F : filter α) (G : filter β) :
filter.map f (F ⊓ filter.comap f G) = filter.map f F ⊓ G
source
@[protected]
theorem filter.push_pull' {α : Type u} {β : Type v} (f : α → β) (F : filter α) (G : filter β) :
filter.map f (filter.comap f G ⊓ F) = G ⊓ filter.map f F
source
theorem filter.singleton_mem_pure {α : Type u} {a : α} :
{a} ∈ pure a
source
theorem filter.pure_injective {α : Type u} :
function.injective pure
source
@[protected, instance]
def filter.pure_ne_bot {α : Type u} {a : α} :
(pure a).ne_bot
source
@[simp]
theorem filter.le_pure_iff {α : Type u} {f : filter α} {a : α} :
f ≤ pure a ↔ {a} ∈ f
source
theorem filter.mem_seq_def {α : Type u} {β : Type v} {f : filter (α → β)} {g : filter α} {s : set β} :
s ∈ f.seq g ↔ ∃ (u : set (α → β)) (H : u ∈ f) (t : set α) (H : t ∈ g), ∀ (x : α → β), x ∈ u → ∀ (y : α), y ∈ t → x y ∈ s
source
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
source
theorem filter.mem_map_seq_iff {α : Type u} {β : Type v} {γ : Type w} {f : filter α} {g : filter β} {m : α → β → γ} {s : set γ} :
s ∈ (filter.map m f).seq g ↔ ∃ (t : set β) (u : set α), t ∈ g ∧ u ∈ f ∧ ∀ (x : α), x ∈ u → ∀ (y : β), y ∈ t → m x y ∈ s
source
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
source
theorem filter.le_seq {α : Type u} {β : Type v} {f : filter (α → β)} {g : filter α} {h : filter β} (hh : ∀ (t : set (α → β)), t ∈ f → ∀ (u : set α), u ∈ g → t.seq u ∈ h) :
h ≤ f.seq g
source
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₂
source
@[simp]
theorem filter.pure_seq_eq_map {α : Type u} {β : Type v} (g : α → β) (f : filter α) :
(pure g).seq f = filter.map g f
source
@[simp]
theorem filter.seq_pure {α : Type u} {β : Type v} (f : filter (α → β)) (a : α) :
f.seq (pure a) = filter.map (λ (g : α → β), g a) f
source
@[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
source
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
source
@[protected, instance]
def filter.is_lawful_functor  :
is_lawful_functor filter
source
@[protected, instance]
def filter.is_lawful_applicative  :
is_lawful_applicative filter
source
@[protected, instance]
def filter.is_comm_applicative  :
is_comm_applicative filter
source
theorem filter.seq_eq_filter_seq {α β : Type l} (f : filter (α → β)) (g : filter α) :
f <*> g = f.seq g

bind equations #

source
@[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
source
@[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₂
source
@[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₂
source
theorem filter.mem_bind' {α : Type u} {β : Type v} {s : set β} {f : filter α} {m : α → filter β} :
s ∈ f.bind m ↔ {a : α | s ∈ m a} ∈ f
source
@[simp]
theorem filter.mem_bind {α : Type u} {β : Type v} {s : set β} {f : filter α} {m : α → filter β} :
s ∈ f.bind m ↔ ∃ (t : set α) (H : t ∈ f), ∀ (x : α), x ∈ t → s ∈ m x
source
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
source
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₂
source
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
source
theorem filter.sup_bind {α : Type u} {β : Type v} {f g : filter α} {h : α → filter β} :
(f ⊔ g).bind h = f.bind h ⊔ g.bind h
source
theorem filter.principal_bind {α : Type u} {β : Type v} {s : set α} {f : α → filter β} :
(𝓟 s).bind f = ⨆ (x : α) (H : x ∈ s), f x
source
theorem filter.sequence_mono {α : Type u} (as bs : list (filter α)) :
list.forall₂ has_le.le as bs → sequence as ≤ sequence bs
source
theorem filter.mem_traverse {α' β' γ' : Type u} {f : β' → filter α'} {s : γ' → set α'} (fs : list β') (us : list γ') :
list.forall₂ (λ (b : β') (c : γ'), s c ∈ f b) fs us → traverse s us ∈ traverse f fs
source
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 #

source
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
source
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₁
source
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))
source
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)
source
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
source
theorem filter.tendsto.frequently_map {α : Type u} {β : Type v} {l₁ : filter α} {l₂ : filter β} {p : α → Prop} {q : β → Prop} (f : α → β) (c : filter.tendsto f l₁ l₂) (w : ∀ (x : α), p x → q (f x)) (h : ∃ᶠ (x : α) in l₁, p x) :
∃ᶠ (y : β) in l₂, q y
source
@[simp]
theorem filter.tendsto_bot {α : Type u} {β : Type v} {f : α → β} {l : filter β} :
filter.tendsto f ⊥ l
source
@[simp]
theorem filter.tendsto_top {α : Type u} {β : Type v} {f : α → β} {l : filter α} :
filter.tendsto f l ⊤
source
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
source
theorem filter.tendsto_of_is_empty {α : Type u} {β : Type v} [is_empty α] {f : α → β} {la : filter α} {lb : filter β} :
filter.tendsto f la lb
source
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₂
source
theorem filter.tendsto_iff_comap {α : Type u} {β : Type v} {f : α → β} {l₁ : filter α} {l₂ : filter β} :
filter.tendsto f l₁ l₂ ↔ l₁ ≤ filter.comap f l₂
source
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.

source
@[protected]
theorem filter.tendsto.disjoint {α : Type u} {β : Type v} {f : α → β} {la₁ la₂ : filter α} {lb₁ lb₂ : filter β} (h₁ : filter.tendsto f la₁ lb₁) (hd : disjoint lb₁ lb₂) (h₂ : filter.tendsto f la₂ lb₂) :
disjoint la₁ la₂
source
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₂
source
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₂
source
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₂
source
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₂
source
theorem filter.tendsto_id' {α : Type u} {x y : filter α} :
x ≤ y → filter.tendsto id x y
source
theorem filter.tendsto_id {α : Type u} {x : filter α} :
filter.tendsto id x x
source
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) :
filter.tendsto (g ∘ f) x z
source
theorem filter.tendsto.mono_left {α : Type u} {β : Type v} {f : α → β} {x y : filter α} {z : filter β} (hx : filter.tendsto f x z) (h : y ≤ x) :
filter.tendsto f y z
source
theorem filter.tendsto.mono_right {α : Type u} {β : Type v} {f : α → β} {x : filter α} {y z : filter β} (hy : filter.tendsto f x y) (hz : y ≤ z) :
filter.tendsto f x z
source
theorem filter.tendsto.ne_bot {α : Type u} {β : Type v} {f : α → β} {x : filter α} {y : filter β} (h : filter.tendsto f x y) [hx : x.ne_bot] :
y.ne_bot
source
theorem filter.tendsto_map {α : Type u} {β : Type v} {f : α → β} {x : filter α} :
filter.tendsto f x (filter.map f x)
source
theorem filter.tendsto_map' {α : Type u} {β : Type v} {γ : Type w} {f : β → γ} {g : α → β} {x : filter α} {y : filter γ} (h : filter.tendsto (f ∘ g) x y) :
filter.tendsto f (filter.map g x) y
source
@[simp]
theorem filter.tendsto_map'_iff {α : Type u} {β : Type v} {γ : Type w} {f : β → γ} {g : α → β} {x : filter α} {y : filter γ} :
filter.tendsto f (filter.map g x) y ↔ filter.tendsto (f ∘ g) x y
source
theorem filter.tendsto_comap {α : Type u} {β : Type v} {f : α → β} {x : filter β} :
filter.tendsto f (filter.comap f x) x
source
@[simp]
theorem filter.tendsto_comap_iff {α : Type u} {β : Type v} {γ : Type w} {f : α → β} {g : β → γ} {a : filter α} {c : filter γ} :
filter.tendsto f a (filter.comap g c) ↔ filter.tendsto (g ∘ f) a c
source
theorem filter.tendsto_comap'_iff {α : Type u} {β : Type v} {γ : Type w} {m : α → β} {f : filter α} {g : filter β} {i : γ → α} (h : set.range i ∈ f) :
filter.tendsto (m ∘ i) (filter.comap i f) g ↔ filter.tendsto m f g
source
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) :
filter.tendsto f a b
source
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) :
filter.comap φ g = f
source
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
source
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₂
source
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
source
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
source
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₂)
source
@[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)
source
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
source
@[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
source
theorem filter.tendsto.sup {α : Type u} {β : Type v} {f : α → β} {x₁ x₂ : filter α} {y : filter β} :
filter.tendsto f x₁ y → filter.tendsto f x₂ y → filter.tendsto f (x₁ ⊔ x₂) y
source
@[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
source
@[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
source
@[simp]
theorem filter.tendsto_principal_principal {α : Type u} {β : Type v} {f : α → β} {s : set α} {t : set β} :
filter.tendsto f (𝓟 s) (𝓟 t) ↔ ∀ (a : α), a ∈ s → f a ∈ t
source
@[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
source
theorem filter.tendsto_pure_pure {α : Type u} {β : Type v} (f : α → β) (a : α) :
filter.tendsto f (pure a) (pure (f a))
source
theorem filter.tendsto_const_pure {α : Type u} {β : Type v} {a : filter α} {b : β} :
filter.tendsto (λ (x : α), b) a (pure b)
source
theorem filter.pure_le_iff {α : Type u} {a : α} {l : filter α} :
pure a ≤ l ↔ ∀ (s : set α), s ∈ l → a ∈ s
source
theorem filter.tendsto_pure_left {α : Type u} {β : Type v} {f : α → β} {a : α} {l : filter β} :
filter.tendsto f (pure a) l ↔ ∀ (s : set β), s ∈ l → f a ∈ s
source
@[simp]
theorem filter.map_inf_principal_preimage {α : Type u} {β : Type v} {f : α → β} {s : set β} {l : filter α} :
filter.map f (l ⊓ 𝓟 (f ⁻¹' s)) = filter.map f l ⊓ 𝓟 s
source
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₂) :
¬filter.tendsto f a b₂

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

source
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₂
source
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 #

source
@[protected]
def filter.prod {α : Type u} {β : Type v} (f : filter α) (g : filter β) :
filter (α × β)

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

Equations
source
theorem filter.prod_mem_prod {α : Type u} {β : Type v} {s : set α} {t : set β} {f : filter α} {g : filter β} (hs : s ∈ f) (ht : t ∈ g) :
s ×ˢ t ∈ f ×ᶠ g
source
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₁ ×ˢ t₂ ⊆ s
source
@[simp]
theorem filter.prod_mem_prod_iff {α : Type u} {β : Type v} {s : set α} {t : set β} {f : filter α} {g : filter β} [f.ne_bot] [g.ne_bot] :
s ×ˢ t ∈ f ×ᶠ g ↔ s ∈ f ∧ t ∈ g
source
theorem filter.mem_prod_principal {α : Type u} {β : Type v} {f : filter α} {s : set (α × β)} {t : set β} :
s ∈ f ×ᶠ 𝓟 t ↔ {a : α | ∀ (b : β), b ∈ t → (a, b) ∈ s} ∈ f
source
theorem filter.mem_prod_top {α : Type u} {β : Type v} {f : filter α} {s : set (α × β)} :
s ∈ f ×ᶠ ⊤ ↔ {a : α | ∀ (b : β), (a, b) ∈ s} ∈ f
source
theorem filter.comap_prod {α : Type u} {β : Type v} {γ : Type w} (f : α → β × γ) (b : filter β) (c : filter γ) :
filter.comap f (b ×ᶠ c) = filter.comap (prod.fst ∘ f) b ⊓ filter.comap (prod.snd ∘ f) c
source
theorem filter.prod_top {α : Type u} {β : Type v} {f : filter α} :
f ×ᶠ ⊤ = filter.comap prod.fst f
source
theorem filter.sup_prod {α : Type u} {β : Type v} (f₁ f₂ : filter α) (g : filter β) :
f₁ ⊔ f₂ ×ᶠ g = (f₁ ×ᶠ g) ⊔ (f₂ ×ᶠ g)
source
theorem filter.prod_sup {α : Type u} {β : Type v} (f : filter α) (g₁ g₂ : filter β) :
f ×ᶠ g₁ ⊔ g₂ = (f ×ᶠ g₁) ⊔ (f ×ᶠ g₂)
source
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 y → p (x, y)
source
theorem filter.tendsto_fst {α : Type u} {β : Type v} {f : filter α} {g : filter β} :
filter.tendsto prod.fst (f ×ᶠ g) f
source
theorem filter.tendsto_snd {α : Type u} {β : Type v} {f : filter α} {g : filter β} :
filter.tendsto prod.snd (f ×ᶠ g) g
source
theorem filter.tendsto.prod_mk {α : Type u} {β : Type v} {γ : Type w} {f : filter α} {g : filter β} {h : filter γ} {m₁ : α → β} {m₂ : α → γ} (h₁ : filter.tendsto m₁ f g) (h₂ : filter.tendsto m₂ f h) :
filter.tendsto (λ (x : α), (m₁ x, m₂ x)) f (g ×ᶠ h)
source
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
source
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
source
theorem filter.eventually.prod_mk {α : Type u} {β : Type v} {la : filter α} {pa : α → Prop} (ha : ∀ᶠ (x : α) in la, pa x) {lb : filter β} {pb : β → Prop} (hb : ∀ᶠ (y : β) in lb, pb y) :
∀ᶠ (p : α × β) in la ×ᶠ lb, pa p.fst ∧ pb p.snd
source
theorem filter.eventually_eq.prod_map {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} {la : filter α} {fa ga : α → γ} (ha : fa =ᶠ[la] ga) {lb : filter β} {fb gb : β → δ} (hb : fb =ᶠ[lb] gb) :
prod.map fa fb =ᶠ[la ×ᶠ lb] prod.map ga gb
source
theorem filter.eventually_le.prod_map {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} [has_le γ] [has_le δ] {la : filter α} {fa ga : α → γ} (ha : fa ≤ᶠ[la] ga) {lb : filter β} {fb gb : β → δ} (hb : fb ≤ᶠ[lb] gb) :
prod.map fa fb ≤ᶠ[la ×ᶠ lb] prod.map ga gb
source
theorem filter.eventually.curry {α : Type u} {β : Type v} {la : filter α} {lb : filter β} {p : α × β → Prop} (h : ∀ᶠ (x : α × β) in la ×ᶠ lb, p x) :
∀ᶠ (x : α) in la, ∀ᶠ (y : β) in lb, p (x, y)
source
theorem filter.prod_infi_left {α : Type u} {β : Type v} {ι : Sort x} [nonempty ι] {f : ι → filter α} {g : filter β} :
(⨅ (i : ι), f i) ×ᶠ g = ⨅ (i : ι), f i ×ᶠ g
source
theorem filter.prod_infi_right {α : Type u} {β : Type v} {ι : Sort x} [nonempty ι] {f : filter α} {g : ι → filter β} :
(f ×ᶠ ⨅ (i : ι), g i) = ⨅ (i : ι), f ×ᶠ g i
source
theorem filter.prod_mono {α : Type u} {β : Type v} {f₁ f₂ : filter α} {g₁ g₂ : filter β} (hf : f₁ ≤ f₂) (hg : g₁ ≤ g₂) :
f₁ ×ᶠ g₁ ≤ f₂ ×ᶠ g₂
source
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₂)
source
theorem filter.prod_comm' {α : Type u} {β : Type v} {f : filter α} {g : filter β} :
f ×ᶠ g = filter.comap prod.swap (g ×ᶠ f)
source
theorem filter.prod_comm {α : Type u} {β : Type v} {f : filter α} {g : filter β} :
f ×ᶠ g = filter.map (λ (p : β × α), (p.snd, p.fst)) (g ×ᶠ f)
source
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₂)
source
theorem filter.prod_map_map_eq' {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} (f : α₁ → α₂) (g : β₁ → β₂) (F : filter α₁) (G : filter β₁) :
filter.map f F ×ᶠ filter.map g G = filter.map (prod.map f g) (F ×ᶠ G)
source
theorem filter.le_prod_map_fst_snd {α : Type u} {β : Type v} {f : filter (α × β)} :
f ≤ filter.map prod.fst f ×ᶠ filter.map prod.snd f
source
theorem filter.tendsto.prod_map {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} {f : α → γ} {g : β → δ} {a : filter α} {b : filter β} {c : filter γ} {d : filter δ} (hf : filter.tendsto f a c) (hg : filter.tendsto g b d) :
filter.tendsto (prod.map f g) (a ×ᶠ b) (c ×ᶠ d)
source
@[protected]
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
source
theorem filter.prod_eq {α : Type u} {β : Type v} {f : filter α} {g : filter β} :
f ×ᶠ g = (filter.map prod.mk f).seq g
source
theorem filter.prod_inf_prod {α : Type u} {β : Type v} {f₁ f₂ : filter α} {g₁ g₂ : filter β} :
(f₁ ×ᶠ g₁) ⊓ (f₂ ×ᶠ g₂) = f₁ ⊓ f₂ ×ᶠ g₁ ⊓ g₂
source
@[simp]
theorem filter.prod_bot {α : Type u} {β : Type v} {f : filter α} :
f ×ᶠ ⊥ = ⊥
source
@[simp]
theorem filter.bot_prod {α : Type u} {β : Type v} {g : filter β} :
⊥ ×ᶠ g = ⊥
source
@[simp]
theorem filter.prod_principal_principal {α : Type u} {β : Type v} {s : set α} {t : set β} :
𝓟 s ×ᶠ 𝓟 t = 𝓟 (s ×ˢ t)
source
@[simp]
theorem filter.pure_prod {α : Type u} {β : Type v} {a : α} {f : filter β} :
pure a ×ᶠ f = filter.map (prod.mk a) f
source
theorem filter.map_pure_prod {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (a : α) (B : filter β) :
filter.map (function.uncurry f) (pure a ×ᶠ B) = filter.map (f a) B
source
@[simp]
theorem filter.prod_pure {α : Type u} {β : Type v} {f : filter α} {b : β} :
f ×ᶠ pure b = filter.map (λ (a : α), (a, b)) f
source
theorem filter.prod_pure_pure {α : Type u} {β : Type v} {a : α} {b : β} :
pure a ×ᶠ pure b = pure (a, b)
source
theorem filter.prod_eq_bot {α : Type u} {β : Type v} {f : filter α} {g : filter β} :
f ×ᶠ g = ⊥ ↔ f = ⊥ ∨ g = ⊥
source
theorem filter.prod_ne_bot {α : Type u} {β : Type v} {f : filter α} {g : filter β} :
(f ×ᶠ g).ne_bot ↔ f.ne_bot ∧ g.ne_bot
source
theorem filter.ne_bot.prod {α : Type u} {β : Type v} {f : filter α} {g : filter β} (hf : f.ne_bot) (hg : g.ne_bot) :
(f ×ᶠ g).ne_bot
source
@[protected, instance]
def filter.prod_ne_bot' {α : Type u} {β : Type v} {f : filter α} {g : filter β} [hf : f.ne_bot] [hg : g.ne_bot] :
(f ×ᶠ g).ne_bot
source
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 ∈ U → y ∈ V → f (x, y) ∈ W)
source
theorem filter.tendsto_prod_iff' {α : Type u} {β : Type v} {γ : Type w} {f : filter α} {g : filter β} {g' : filter γ} {s : α → β × γ} :
filter.tendsto s f (g ×ᶠ g') ↔ filter.tendsto (λ (n : α), (s n).fst) f g ∧ filter.tendsto (λ (n : α), (s n).snd) f g'

Coproducts of filters #

source
@[protected]
def filter.coprod {α : Type u} {β : Type v} (f : filter α) (g : filter β) :
filter (α × β)

Coproduct of filters.

Equations
source
theorem filter.mem_coprod_iff {α : Type u} {β : Type v} {s : set (α × β)} {f : filter α} {g : filter β} :
s ∈ f.coprod g ↔ (∃ (t₁ : set α) (H : t₁ ∈ f), prod.fst ⁻¹' t₁ ⊆ s) ∧ ∃ (t₂ : set β) (H : t₂ ∈ g), prod.snd ⁻¹' t₂ ⊆ s
source
theorem filter.coprod_mono {α : Type u} {β : Type v} {f₁ f₂ : filter α} {g₁ g₂ : filter β} (hf : f₁ ≤ f₂) (hg : g₁ ≤ g₂) :
f₁.coprod g₁ ≤ f₂.coprod g₂
source
theorem filter.coprod_ne_bot_iff {α : Type u} {β : Type v} {f : filter α} {g : filter β} :
(f.coprod g).ne_bot ↔ f.ne_bot ∧ nonempty β ∨ nonempty α ∧ g.ne_bot
source
@[instance]
theorem filter.coprod_ne_bot_left {α : Type u} {β : Type v} {f : filter α} {g : filter β} [f.ne_bot] [nonempty β] :
(f.coprod g).ne_bot
source
@[instance]
theorem filter.coprod_ne_bot_right {α : Type u} {β : Type v} {f : filter α} {g : filter β} [g.ne_bot] [nonempty α] :
(f.coprod g).ne_bot
source
theorem filter.principal_coprod_principal {α : Type u} {β : Type v} (s : set α) (t : set β) :
(𝓟 s).coprod (𝓟 t) = 𝓟 (sᶜ ×ˢ tᶜ)ᶜ
source
theorem filter.map_prod_map_coprod_le {α₁ : Type u} {α₂ : Type v} {β₁ : Type w} {β₂ : Type x} {f₁ : filter α₁} {f₂ : filter α₂} {m₁ : α₁ → β₁} {m₂ : α₂ → β₂} :
filter.map (prod.map m₁ m₂) (f₁.coprod f₂) ≤ (filter.map m₁ f₁).coprod (filter.map m₂ f₂)
source
theorem filter.map_const_principal_coprod_map_id_principal {α : Type u_1} {β : Type u_2} {ι : Type u_3} (a : α) (b : β) (i : ι) :
(filter.map (λ (_x : α), b) (𝓟 {a})).coprod (filter.map id (𝓟 {i})) = 𝓟 ({b} ×ˢ set.univ ∪ set.univ ×ˢ {i})

Characterization of the coproduct of the filter.maps of two principal filters 𝓟 {a} and 𝓟 {i}, the first under the constant function λ a, b and the second under the identity function. Together with the next lemma, map_prod_map_const_id_principal_coprod_principal, this provides an example showing that the inequality in the lemma map_prod_map_coprod_le can be strict.

source
theorem filter.map_prod_map_const_id_principal_coprod_principal {α : Type u_1} {β : Type u_2} {ι : Type u_3} (a : α) (b : β) (i : ι) :
filter.map (prod.map (λ (_x : α), b) id) ((𝓟 {a}).coprod (𝓟 {i})) = 𝓟 ({b} ×ˢ set.univ)

Characterization of the filter.map of the coproduct of two principal filters 𝓟 {a} and 𝓟 {i}, under the prod.map of two functions, respectively the constant function λ a, b and the identity function. Together with the previous lemma, map_const_principal_coprod_map_id_principal, this provides an example showing that the inequality in the lemma map_prod_map_coprod_le can be strict.

source
theorem filter.tendsto.prod_map_coprod {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} {f : α → γ} {g : β → δ} {a : filter α} {b : filter β} {c : filter γ} {d : filter δ} (hf : filter.tendsto f a c) (hg : filter.tendsto g b d) :
filter.tendsto (prod.map f g) (a.coprod b) (c.coprod d)
source
theorem set.eq_on.eventually_eq {α : Type u_1} {β : Type u_2} {s : set α} {f g : α → β} (h : set.eq_on f g s) :
f =ᶠ[𝓟 s] g
source
theorem set.eq_on.eventually_eq_of_mem {α : Type u_1} {β : Type u_2} {s : set α} {l : filter α} {f g : α → β} (h : set.eq_on f g s) (hl : s ∈ l) :
f =ᶠ[l] g
source
theorem set.subset.eventually_le {α : Type u_1} {l : filter α} {s t : set α} (h : s ⊆ t) :
s ≤ᶠ[l] t
source
theorem set.maps_to.tendsto {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {f : α → β} (h : set.maps_to f s t) :
filter.tendsto f (𝓟 s) (𝓟 t)