mathlib3 documentation

order.filter.basic

Theory of filters on sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main definitions #

Filters on a type X are sets of sets of X satisfying three conditions. They are mostly used to abstract two related kinds of ideas:

In this file, we define the type filter X of filters on X, and endow it with a complete lattice structure. This structure is lifted from the lattice structure on set (set X) using the Galois insertion which maps a filter to its elements in one direction, and an arbitrary set of sets to the smallest filter containing it in the other direction. We also prove filter is a monadic functor, with a push-forward operation filter.map and a pull-back operation filter.comap that form a Galois connections for the order on filters.

The examples of filters appearing in the description of the two motivating ideas are:

The general notion of limit of a map with respect to filters on the source and target types is filter.tendsto. It is defined in terms of the order and the push-forward operation. The predicate "happening eventually" is filter.eventually, and "happening often" is filter.frequently, whose definitions are immediate after filter is defined (but they come rather late in this file in order to immediately relate them to the lattice structure).

For instance, anticipating on topology.basic, the statement: "if a sequence u converges to some x and u n belongs to a set M for n large enough then x is in the closure of M" is formalized as: tendsto u at_top (𝓝 x) → (∀ᶠ n in at_top, u n ∈ M) → x ∈ closure M, which is a special case of mem_closure_of_tendsto from topology.basic.

Notations #

References #

Important note: Bourbaki requires that a filter on X cannot contain all sets of X, which we do not require. This gives filter X better formal properties, in particular a bottom element ⊥ for its lattice structure, at the cost of including the assumption [ne_bot f] in a number of lemmas and definitions.

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

Instances for filter
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
@[protected]
theorem filter.coext {α : Type u} {f g : filter α} (h : ∀ (s : set α), sᶜ ∈ f ↔ sᶜ ∈ g) :
f = g

An extensionality lemma that is useful for filters with good lemmas about sᶜ ∈ f (e.g., filter.comap, filter.coprod, filter.Coprod, filter.cofinite).

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 filter.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 α} [finite β] :
(⋂ (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 (optional interactive.types.pexpr_list)) (wth : interactive.parse (optional interactive.types.with_ident_list)) (tgt : interactive.parse (optional (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 tactic_doc.tactic.filter_upwards  :
tactic_doc_entry

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
Instances for filter.principal
source
@[simp]
theorem filter.mem_principal {α : Type u} {s t : set α} :
s ∈ filter.principal t ↔ t ⊆ s
source
theorem filter.mem_principal_self {α : Type u} (s : set α) :
s ∈ filter.principal 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
@[protected]
theorem filter.not_le {α : Type u} {f g : filter α} :
¬f ≤ g ↔ ∃ (s : set α) (H : s ∈ g), s ∉ 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
@[protected, instance]
def filter.inhabited {α : Type u} :
inhabited (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 of this typeclass
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.not_disjoint_self_iff {α : Type u} {f : filter α} :
¬disjoint f f ↔ f.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 α)} :
(has_Sup.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 ∈ has_Sup.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_finite {ι : Type u_1} [finite ι] {α : Type u_2} {f : ι → filter α} (s : set α) :
(s ∈ ⨅ (i : ι), f i) ↔ ∃ (t : ι → set α), (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ (i : ι), t i
source
@[simp]
theorem filter.le_principal_iff {α : Type u} {s : set α} {f : filter α} :
f ≤ filter.principal s ↔ s ∈ f
source
theorem filter.Iic_principal {α : Type u} (s : set α) :
set.Iic (filter.principal s) = {l : filter α | s ∈ l}
source
theorem filter.principal_mono {α : Type u} {s t : set α} :
filter.principal s ≤ filter.principal t ↔ s ⊆ t
source
theorem filter.monotone_principal {α : Type u} :
monotone filter.principal
source
@[simp]
theorem filter.principal_eq_iff_eq {α : Type u} {s t : set α} :
filter.principal s = filter.principal t ↔ s = t
source
@[simp]
theorem filter.join_principal_eq_Sup {α : Type u} {s : set (filter α)} :
(filter.principal s).join = has_Sup.Sup s
source
@[simp]
theorem filter.principal_univ {α : Type u} :
filter.principal set.univ = ⊤
source
@[simp]
theorem filter.principal_empty {α : Type u} :
filter.principal ∅ = ⊥
source
theorem filter.generate_eq_binfi {α : Type u} (S : set (set α)) :
filter.generate S = ⨅ (s : set α) (H : s ∈ S), filter.principal 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.ne_bot.not_disjoint {α : Type u} {f : filter α} {s t : set α} (hf : f.ne_bot) (hs : s ∈ f) (ht : t ∈ f) :
¬disjoint s t
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
theorem pairwise.exists_mem_filter_of_disjoint {α : Type u} {ι : Type u_1} [finite ι] {l : ι → filter α} (hd : pairwise (disjoint on l)) :
∃ (s : ι → set α), (∀ (i : ι), s i ∈ l i) ∧ pairwise (disjoint on s)
source
theorem set.pairwise_disjoint.exists_mem_filter {α : Type u} {ι : Type u_1} {l : ι → filter α} {t : set ι} (hd : t.pairwise_disjoint l) (ht : t.finite) :
∃ (s : ι → set α), (∀ (i : ι), s i ∈ l i) ∧ t.pairwise_disjoint s
source
@[protected, instance]
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
@[protected, instance]
def filter.nontrivial {α : Type u} [nonempty α] :
nontrivial (filter α)
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 = has_Inf.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.Inf_ne_bot_of_directed' {α : Type u} {s : set (filter α)} (hne : s.nonempty) (hd : directed_on ge s) (hbot : ⊥ ∉ s) :
(has_Inf.Inf s).ne_bot
source
theorem filter.Inf_ne_bot_of_directed {α : Type u} [nonempty α] {s : set (filter α)} (hd : directed_on ge s) (hbot : ⊥ ∉ s) :
(has_Inf.Inf s).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_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 α} :
filter.principal s ⊓ filter.principal t = filter.principal (s ∩ t)
source
@[simp]
theorem filter.sup_principal {α : Type u} {s t : set α} :
filter.principal s ⊔ filter.principal t = filter.principal (s ∪ t)
source
@[simp]
theorem filter.supr_principal {α : Type u} {ι : Sort w} {s : ι → set α} :
(⨆ (x : ι), filter.principal (s x)) = filter.principal (⋃ (i : ι), s i)
source
@[simp]
theorem filter.principal_eq_bot_iff {α : Type u} {s : set α} :
filter.principal s = ⊥ ↔ s = ∅
source
@[simp]
theorem filter.principal_ne_bot_iff {α : Type u} {s : set α} :
(filter.principal s).ne_bot ↔ s.nonempty
source
theorem set.nonempty.principal_ne_bot {α : Type u} {s : set α} :
s.nonempty → (filter.principal s).ne_bot

Alias of the reverse direction of filter.principal_ne_bot_iff.

source
theorem filter.is_compl_principal {α : Type u} (s : set α) :
is_compl (filter.principal s) (filter.principal sᶜ)
source
theorem filter.mem_inf_principal' {α : Type u} {f : filter α} {s t : set α} :
s ∈ f ⊓ filter.principal t ↔ tᶜ ∪ s ∈ f
source
theorem filter.mem_inf_principal {α : Type u} {f : filter α} {s t : set α} :
s ∈ f ⊓ filter.principal t ↔ {x : α | x ∈ t → x ∈ s} ∈ f
source
theorem filter.supr_inf_principal {α : Type u} {ι : Sort x} (f : ι → filter α) (s : set α) :
(⨆ (i : ι), f i ⊓ filter.principal s) = (⨆ (i : ι), f i) ⊓ filter.principal s
source
theorem filter.inf_principal_eq_bot {α : Type u} {f : filter α} {s : set α} :
f ⊓ filter.principal s = ⊥ ↔ sᶜ ∈ f
source
theorem filter.mem_of_eq_bot {α : Type u} {f : filter α} {s : set α} (h : f ⊓ filter.principal 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 ⊓ filter.principal tᶜ
source
theorem filter.principal_le_iff {α : Type u} {s : set α} {f : filter α} :
filter.principal 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), filter.principal (f i)) = filter.principal (⋂ (i : ι) (H : i ∈ s), f i)
source
@[simp]
theorem filter.infi_principal {α : Type u} {ι : Type w} [finite ι] (f : ι → set α) :
(⨅ (i : ι), filter.principal (f i)) = filter.principal (⋂ (i : ι), f i)
source
theorem filter.infi_principal_finite {α : Type u} {ι : Type w} {s : set ι} (hs : s.finite) (f : ι → set α) :
(⨅ (i : ι) (H : i ∈ s), filter.principal (f i)) = filter.principal (⋂ (i : ι) (H : i ∈ s), f i)
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
Instances for filter.eventually
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
theorem filter.forall_eventually_of_eventually_forall {α : Type u} {β : Type v} {f : filter α} {p : α → β → Prop} (h : ∀ᶠ (x : α) in f, ∀ (y : β), p x y) (y : β) :
∀ᶠ (x : α) in f, p x y
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} [finite ι] {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 filter.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 filter.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 has_Sup.Sup fs, p x) ↔ ∀ (f : filter α), f ∈ fs → (∀ᶠ (x : α) in f, p x)
source
@[simp]
theorem filter.eventually_supr {α : Type u} {ι : Sort x} {p : α → Prop} {fs : ι → filter α} :
(∀ᶠ (x : α) in ⨆ (b : ι), fs b, p x) ↔ ∀ (b : ι), ∀ᶠ (x : α) in fs b, p x
source
@[simp]
theorem filter.eventually_principal {α : Type u} {a : set α} {p : α → Prop} :
(∀ᶠ (x : α) in filter.principal 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 ⊓ filter.principal 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 filter.principal 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 has_Sup.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
source
theorem filter.eventually.choice {α : Type u} {β : Type v} {r : α → β → Prop} {l : filter α} [l.ne_bot] (h : ∀ᶠ (x : α) in l, ∃ (y : β), r x y) :
∃ (f : α → β), ∀ᶠ (x : α) in l, r x (f x)

Relation “eventually equal” #

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
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 the reverse direction of filter.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 the forward direction of filter.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
@[refl]
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
@[symm]
theorem filter.eventually_eq.symm {α : Type u} {β : Type v} {f g : α → β} {l : filter α} (H : f =ᶠ[l] g) :
g =ᶠ[l] f
source
@[trans]
theorem filter.eventually_eq.trans {α : Type u} {β : Type v} {l : filter α} {f g h : α → β} (H₁ : f =ᶠ[l] g) (H₂ : g =ᶠ[l] h) :
f =ᶠ[l] h
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_smul 𝕜 β] {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_smul 𝕜 β] {l : filter α} {f f' : α → 𝕜} {g g' : α → β} (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') :
(λ (x : α), f x • g x) =ᶠ[l] λ (x : α), f' x • g' x
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 =ᶠ[filter.principal 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 ⊓ filter.principal 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
@[refl]
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
@[trans]
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
@[trans]
theorem filter.eventually_eq.trans_le {α : Type u} {β : Type v} [preorder β] {l : filter α} {f g h : α → β} (H₁ : f =ᶠ[l] g) (H₂ : g ≤ᶠ[l] h) :
f ≤ᶠ[l] h
source
@[trans]
theorem filter.eventually_le.trans_eq {α : Type u} {β : Type v} [preorder β] {l : filter α} {f g h : α → β} (H₁ : f ≤ᶠ[l] g) (H₂ : g =ᶠ[l] h) :
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.set_eventually_le_iff_mem_inf_principal {α : Type u} {s t : set α} {l : filter α} :
s ≤ᶠ[l] t ↔ t ∈ l ⊓ filter.principal s
source
theorem filter.set_eventually_le_iff_inf_principal_le {α : Type u} {s t : set α} {l : filter α} :
s ≤ᶠ[l] t ↔ l ⊓ filter.principal s ≤ l ⊓ filter.principal t
source
theorem filter.set_eventually_eq_iff_inf_principal {α : Type u} {s t : set α} {l : filter α} :
s =ᶠ[l] t ↔ l ⊓ filter.principal s = l ⊓ filter.principal t
source
theorem filter.eventually_le.mul_le_mul {α : Type u} {β : Type v} [mul_zero_class β] [partial_order β] [pos_mul_mono β] [mul_pos_mono β] {l : filter α} {f₁ f₂ g₁ g₂ : α → β} (hf : f₁ ≤ᶠ[l] f₂) (hg : g₁ ≤ᶠ[l] g₂) (hg₀ : 0 ≤ᶠ[l] g₁) (hf₀ : 0 ≤ᶠ[l] f₂) :
f₁ * g₁ ≤ᶠ[l] f₂ * g₂
source
theorem eventually_le.add_le_add {α : Type u} {β : Type v} [has_add β] [preorder β] [covariant_class β β has_add.add has_le.le] [covariant_class β β (function.swap has_add.add) has_le.le] {l : filter α} {f₁ f₂ g₁ g₂ : α → β} (hf : f₁ ≤ᶠ[l] f₂) (hg : g₁ ≤ᶠ[l] g₂) :
f₁ + g₁ ≤ᶠ[l] f₂ + g₂
source
theorem filter.eventually_le.mul_le_mul' {α : Type u} {β : Type v} [has_mul β] [preorder β] [covariant_class β β has_mul.mul has_le.le] [covariant_class β β (function.swap has_mul.mul) has_le.le] {l : filter α} {f₁ f₂ g₁ g₂ : α → β} (hf : f₁ ≤ᶠ[l] f₂) (hg : g₁ ≤ᶠ[l] g₂) :
f₁ * g₁ ≤ᶠ[l] f₂ * g₂
source
theorem filter.eventually_le.mul_nonneg {α : Type u} {β : Type v} [ordered_semiring β] {l : filter α} {f g : α → β} (hf : 0 ≤ᶠ[l] f) (hg : 0 ≤ᶠ[l] g) :
0 ≤ᶠ[l] f * g
source
theorem filter.eventually_sub_nonneg {α : Type u} {β : Type v} [ordered_ring β] {l : filter α} {f g : α → β} :
0 ≤ᶠ[l] g - f ↔ f ≤ᶠ[l] g
source
theorem filter.eventually_le.sup {α : Type u} {β : Type v} [semilattice_sup β] {l : filter α} {f₁ f₂ g₁ g₂ : α → β} (hf : f₁ ≤ᶠ[l] f₂) (hg : g₁ ≤ᶠ[l] g₂) :
f₁ ⊔ g₁ ≤ᶠ[l] f₂ ⊔ g₂
source
theorem filter.eventually_le.sup_le {α : Type u} {β : Type v} [semilattice_sup β] {l : filter α} {f g h : α → β} (hf : f ≤ᶠ[l] h) (hg : g ≤ᶠ[l] h) :
f ⊔ g ≤ᶠ[l] h
source
theorem filter.eventually_le.le_sup_of_le_left {α : Type u} {β : Type v} [semilattice_sup β] {l : filter α} {f g h : α → β} (hf : h ≤ᶠ[l] f) :
h ≤ᶠ[l] f ⊔ g
source
theorem filter.eventually_le.le_sup_of_le_right {α : Type u} {β : Type v} [semilattice_sup β] {l : filter α} {f g h : α → β} (hg : h ≤ᶠ[l] g) :
h ≤ᶠ[l] f ⊔ g
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
Instances for filter.map
source
@[simp]
theorem filter.map_principal {α : Type u} {β : Type v} {s : set α} {f : α → β} :
filter.map f (filter.principal s) = filter.principal (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. A set s belongs to filter.comap m f if either of the following equivalent conditions hold.

  1. There exists a set t ∈ f such that m ⁻¹' t ⊆ s. This is used as a definition.
  2. The set {y | ∀ x, m x = y → x ∈ s} belongs to f, see filter.mem_comap'.
  3. The set (m '' sᶜ)ᶜ belongs to f, see filter.mem_comap_iff_compl and filter.compl_mem_comap.
Equations
Instances for filter.comap
source
theorem filter.mem_comap' {α : Type u} {β : Type v} {f : α → β} {l : filter β} {s : set α} :
s ∈ filter.comap f l ↔ {y : β | ∀ ⦃x : α⦄, f x = y → x ∈ s} ∈ l
source
theorem filter.mem_comap_prod_mk {α : Type u} {β : Type v} {x : α} {s : set β} {F : filter (α × β)} :
s ∈ filter.comap (prod.mk x) F ↔ {p : α × β | p.fst = x → p.snd ∈ s} ∈ F

RHS form is used, e.g., in the definition of uniform_space.

source
@[simp]
theorem filter.eventually_comap {α : Type u} {β : Type v} {f : α → β} {l : filter β} {p : α → Prop} :
(∀ᶠ (a : α) in filter.comap f l, p a) ↔ ∀ᶠ (b : β) in l, ∀ (a : α), f a = b → p a
source
@[simp]
theorem filter.frequently_comap {α : Type u} {β : Type v} {f : α → β} {l : filter β} {p : α → Prop} :
(∃ᶠ (a : α) in filter.comap f l, p a) ↔ ∃ᶠ (b : β) in l, ∃ (a : α), f a = b ∧ p a
source
theorem filter.mem_comap_iff_compl {α : Type u} {β : Type v} {f : α → β} {l : filter β} {s : set α} :
s ∈ filter.comap f l ↔ (f '' sᶜ)ᶜ ∈ l
source
theorem filter.compl_mem_comap {α : Type u} {β : Type v} {f : α → β} {l : filter β} {s : set α} :
sᶜ ∈ filter.comap f l ↔ (f '' s)ᶜ ∈ l
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 : α) :
(has_pure.pure a).sets = {s : set α | a ∈ s}
source
@[simp]
theorem filter.mem_pure {α : Type u} {a : α} {s : set α} :
s ∈ has_pure.pure a ↔ a ∈ s
source
@[simp]
theorem filter.eventually_pure {α : Type u} {a : α} {p : α → Prop} :
(∀ᶠ (x : α) in has_pure.pure a, p x) ↔ p a
source
@[simp]
theorem filter.principal_singleton {α : Type u} (a : α) :
filter.principal {a} = has_pure.pure a
source
@[simp]
theorem filter.map_pure {α : Type u} {β : Type v} (f : α → β) (a : α) :
filter.map f (has_pure.pure a) = has_pure.pure (f a)
source
@[simp]
theorem filter.join_pure {α : Type u} (f : filter α) :
(has_pure.pure f).join = f
source
@[simp]
theorem filter.pure_bind {α : Type u} {β : Type v} (a : α) (m : α → filter β) :
(has_pure.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.eventually.comap {α : Type u} {β : Type v} {g : filter β} {p : β → Prop} (hf : ∀ᶠ (b : β) in g, p b) (f : α → β) :
∀ᶠ (a : α) in filter.comap f g, p (f a)
source
theorem filter.comap_id {α : Type u} {f : filter α} :
filter.comap id f = f
source
theorem filter.comap_id' {α : Type u} {f : filter α} :
filter.comap (λ (x : α), x) 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 = has_pure.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
theorem function.semiconj.filter_map {α : Type u} {β : Type v} {f : α → β} {ga : α → α} {gb : β → β} (h : function.semiconj f ga gb) :
function.semiconj (filter.map f) (filter.map ga) (filter.map gb)
source
theorem function.commute.filter_map {α : Type u} {f g : α → α} (h : function.commute f g) :
function.commute (filter.map f) (filter.map g)
source
theorem function.semiconj.filter_comap {α : Type u} {β : Type v} {f : α → β} {ga : α → α} {gb : β → β} (h : function.semiconj f ga gb) :
function.semiconj (filter.comap f) (filter.comap gb) (filter.comap ga)
source
theorem function.commute.filter_comap {α : Type u} {f g : α → α} (h : function.commute f g) :
function.commute (filter.comap f) (filter.comap g)
source
@[simp]
theorem filter.comap_principal {α : Type u} {β : Type v} {m : α → β} {t : set β} :
filter.comap m (filter.principal t) = filter.principal (m ⁻¹' t)
source
@[simp]
theorem filter.comap_pure {α : Type u} {β : Type v} {m : α → β} {b : β} :
filter.comap m (has_pure.pure b) = filter.principal (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.map_top {α : Type u} {β : Type v} (f : α → β) :
filter.map f ⊤ = filter.principal (set.range f)
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.ne_bot_of_comap {α : Type u} {β : Type v} {g : filter β} {m : α → β} (h : (filter.comap m g).ne_bot) :
g.ne_bot
source
theorem filter.comap_inf_principal_range {α : Type u} {β : Type v} {g : filter β} {m : α → β} :
filter.comap m (g ⊓ filter.principal (set.range m)) = filter.comap m g
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 (has_Sup.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 ⊓ filter.principal (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} (c : out_param (β → α)) (p : out_param (α → Prop)) [can_lift α β c p] :
can_lift (filter α) (filter β) (filter.map c) (λ (f : filter α), ∀ᶠ (x : α) in f, p x)
Equations
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 ⊓ filter.principal 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.map_le_map_iff_of_inj_on {α : Type u} {β : Type v} {l₁ l₂ : filter α} {f : α → β} {s : set α} (h₁ : s ∈ l₁) (h₂ : s ∈ l₂) (hinj : set.inj_on f s) :
filter.map f l₁ ≤ filter.map f l₂ ↔ l₁ ≤ l₂
source
theorem filter.map_le_map_iff {α : Type u} {β : Type v} {f g : filter α} {m : α → β} (hm : function.injective m) :
filter.map m f ≤ filter.map m g ↔ f ≤ g
source
theorem filter.map_eq_map_iff_of_inj_on {α : Type u} {β : Type v} {f g : filter α} {m : α → β} {s : set α} (hsf : s ∈ f) (hsg : s ∈ g) (hm : set.inj_on m s) :
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) :
filter.map m f = filter.map m g ↔ f = g
source
theorem filter.map_injective {α : Type u} {β : Type v} {m : α → β} (hm : function.injective m) :
function.injective (filter.map m)
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.comap_eq_bot_iff_compl_range {α : Type u} {β : Type v} {f : filter β} {m : α → β} :
filter.comap m f = ⊥ ↔ (set.range m)ᶜ ∈ f
source
theorem filter.comap_surjective_eq_bot {α : Type u} {β : Type v} {f : filter β} {m : α → β} (hm : function.surjective m) :
filter.comap m f = ⊥ ↔ f = ⊥
source
theorem filter.disjoint_comap_iff {α : Type u} {β : Type v} {g₁ g₂ : filter β} {m : α → β} (h : function.surjective m) :
disjoint (filter.comap m g₁) (filter.comap m g₂) ↔ disjoint g₁ g₂
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 ⊓ filter.principal 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 ≤ filter.principal 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
theorem filter.ne_bot.of_map {α : Type u} {β : Type v} {f : filter α} {m : α → β} :
(filter.map m f).ne_bot → 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_equiv_symm {α : Type u} {β : Type v} (e : α ≃ β) (f : filter β) :
filter.map ⇑(e.symm) f = filter.comap ⇑e 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.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.map_swap4_eq_comap {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} {f : filter ((α × β) × γ × δ)} :
filter.map (λ (p : (α × β) × γ × δ), ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) f = filter.comap (λ (p : (α × γ) × β × δ), ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) f

A useful lemma when dealing with uniformities.

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
theorem filter.le_map_iff {α : Type u} {β : Type v} {f : filter α} {m : α → β} {g : filter β} :
g ≤ filter.map m f ↔ ∀ (s : set α), s ∈ f → m '' s ∈ g
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.principal_eq_map_coe_top {α : Type u} (s : set α) :
filter.principal s = filter.map coe ⊤
source
theorem filter.inf_principal_eq_bot_iff_comap {α : Type u} {F : filter α} {s : set α} :
F ⊓ filter.principal s = ⊥ ↔ filter.comap coe F = ⊥
source
theorem filter.singleton_mem_pure {α : Type u} {a : α} :
{a} ∈ has_pure.pure a
source
theorem filter.pure_injective {α : Type u} :
function.injective has_pure.pure
source
@[protected, instance]
def filter.pure_ne_bot {α : Type u} {a : α} :
(has_pure.pure a).ne_bot
source
@[simp]
theorem filter.le_pure_iff {α : Type u} {f : filter α} {a : α} :
f ≤ has_pure.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 α) :
(has_pure.pure g).seq f = filter.map g f
source
@[simp]
theorem filter.seq_pure {α : Type u} {β : Type v} (f : filter (α → β)) (a : α) :
f.seq (has_pure.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 ⊓ filter.principal s) = f.bind g ⊓ filter.principal 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 β} :
(filter.principal 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 → traversable.traverse s us ∈ traversable.traverse f fs
source
theorem filter.mem_traverse_iff {α' β' : Type u} {f : β' → filter α'} (fs : list β') (t : set (list α')) :
t ∈ traversable.traverse f fs ↔ ∃ (us : list (set α')), list.forall₂ (λ (b : β') (s : set α'), s ∈ f b) fs us ∧ sequence us ⊆ t

Limits #

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 the forward direction of filter.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 α} :
filter.tendsto id x y ↔ 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
theorem filter.tendsto_infi_infi {α : Type u} {β : Type v} {ι : Sort x} {f : α → β} {x : ι → filter α} {y : ι → filter β} (h : ∀ (i : ι), filter.tendsto f (x i) (y i)) :
filter.tendsto f (infi x) (infi 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
theorem filter.tendsto_supr_supr {α : Type u} {β : Type v} {ι : Sort x} {f : α → β} {x : ι → filter α} {y : ι → filter β} (h : ∀ (i : ι), filter.tendsto f (x i) (y i)) :
filter.tendsto f (supr x) (supr y)
source
@[simp]
theorem filter.tendsto_principal {α : Type u} {β : Type v} {f : α → β} {l : filter α} {s : set β} :
filter.tendsto f l (filter.principal s) ↔ ∀ᶠ (a : α) in l, f a ∈ s
source
@[simp]
theorem filter.tendsto_principal_principal {α : Type u} {β : Type v} {f : α → β} {s : set α} {t : set β} :
filter.tendsto f (filter.principal s) (filter.principal 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 (has_pure.pure b) ↔ ∀ᶠ (x : α) in a, f x = b
source
theorem filter.tendsto_pure_pure {α : Type u} {β : Type v} (f : α → β) (a : α) :
filter.tendsto f (has_pure.pure a) (has_pure.pure (f a))
source
theorem filter.tendsto_const_pure {α : Type u} {β : Type v} {a : filter α} {b : β} :
filter.tendsto (λ (x : α), b) a (has_pure.pure b)
source
theorem filter.pure_le_iff {α : Type u} {a : α} {l : filter α} :
has_pure.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 (has_pure.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 ⊓ filter.principal (f ⁻¹' s)) = filter.map f l ⊓ filter.principal 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
@[protected]
theorem filter.tendsto.if {α : Type u} {β : Type v} {l₁ : filter α} {l₂ : filter β} {f g : α → β} {p : α → Prop} [Π (x : α), decidable (p x)] (h₀ : filter.tendsto f (l₁ ⊓ filter.principal {x : α | p x}) l₂) (h₁ : filter.tendsto g (l₁ ⊓ filter.principal {x : α | ¬p x}) l₂) :
filter.tendsto (λ (x : α), ite (p x) (f x) (g x)) l₁ l₂
source
@[protected]
theorem filter.tendsto.if' {α : Type u_1} {β : Type u_2} {l₁ : filter α} {l₂ : filter β} {f g : α → β} {p : α → Prop} [decidable_pred p] (hf : filter.tendsto f l₁ l₂) (hg : filter.tendsto g l₁ l₂) :
filter.tendsto (λ (a : α), ite (p a) (f a) (g a)) l₁ l₂
source
@[protected]
theorem filter.tendsto.piecewise {α : Type u} {β : Type v} {l₁ : filter α} {l₂ : filter β} {f g : α → β} {s : set α} [Π (x : α), decidable (x ∈ s)] (h₀ : filter.tendsto f (l₁ ⊓ filter.principal s) l₂) (h₁ : filter.tendsto g (l₁ ⊓ filter.principal sᶜ) l₂) :
filter.tendsto (s.piecewise f g) l₁ l₂
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 =ᶠ[filter.principal 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 has_subset.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 (filter.principal s) (filter.principal t)