mathlib docs: order.filter.basic

structure filter :

Type u_1 → Type u_1

sets : set (set α)
univ_sets : set.univ ∈ c.sets
sets_of_superset : ∀ {x y : set α}, x ∈ c.sets → x ⊆ y → y ∈ c.sets
inter_sets : ∀ {x y : set α}, x ∈ c.sets → y ∈ c.sets → x ∩ y ∈ c.sets

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

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

filter.has_mem = {mem := λ (U : set α) (F : filter α), U ∈ F.sets}

source

@[instance]

def filter.inhabited_mem {α : Type u} {f : filter α} :

inhabited {s // s ∈ f}

Equations

filter.inhabited_mem = {default := ⟨set.univ α, _⟩}

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

theorem filter.ext_iff {α : Type u} {f g : filter α} :

f = g ↔ ∀ (s : set α), s ∈ f ↔ s ∈ g

source

@[ext]

theorem filter.ext {α : Type u} {f g : filter α} :

(∀ (s : set α), s ∈ f ↔ s ∈ g) → f = g

source

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

set.univ ∈ f

source

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

x ∈ f → x ⊆ y → y ∈ f

source

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

s ∈ f → t ∈ f → s ∩ t ∈ f

source

theorem filter.univ_mem_sets' {α : Type u} {f : filter α} {s : set α} :

(∀ (a : α), a ∈ s) → s ∈ f

source

theorem filter.mp_sets {α : Type u} {f : filter α} {s t : set α} :

s ∈ f → {x : α | x ∈ s → x ∈ t} ∈ f → t ∈ f

source

theorem filter.congr_sets {α : Type u} {f : filter α} {s t : set α} :

{x : α | x ∈ s ↔ x ∈ t} ∈ f → (s ∈ f ↔ t ∈ f)

source

theorem filter.Inter_mem_sets {α : Type u} {f : filter α} {β : Type v} {s : β → set α} {is : set β} :

is.finite → (∀ (i : β), i ∈ is → s i ∈ f) → (⋂ (i : β) (H : i ∈ is), s i) ∈ f

source

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

s.finite → (∀ (U : set α), U ∈ s → U ∈ f) → ⋂₀s ∈ f

source

theorem filter.Inter_mem_sets_of_fintype {α : Type u} {f : filter α} {β : Type v} {s : β → set α} [fintype β] :

(∀ (i : β), s i ∈ f) → (⋂ (i : β), s i) ∈ f

source

theorem filter.exists_sets_subset_iff {α : Type u} {f : filter α} {s : set α} :

(∃ (t : set α) (H : t ∈ f), t ⊆ s) ↔ s ∈ f

source

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

monotone (λ (s : set α), s ∈ f)

source

meta def tactic.interactive.filter_upwards :

interactive.parse interactive.types.pexpr_list → interactive.parse (optional interactive.types.texpr) → tactic unit

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

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

source

def filter.principal {α : Type u} :

set α → filter α

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

Equations

filter.principal s = {sets := {t : set α | s ⊆ t}, univ_sets := _, sets_of_superset := _, inter_sets := _}

source

@[instance]

def filter.inhabited {α : Type u} :

inhabited (filter α)

Equations

filter.inhabited = {default := filter.principal ∅}

source

@[simp]

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

filter (filter α) → filter α

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

Equations

f.join = {sets := {s : set α | {t : filter α | s ∈ t} ∈ f}, univ_sets := _, sets_of_superset := _, inter_sets := _}

source

@[simp]

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

s ∈ f.join ↔ {t : filter α | s ∈ t} ∈ f

source

@[instance]

def filter.partial_order {α : Type u} :

partial_order (filter α)

Equations

filter.partial_order = {le := λ (f g : filter α), ∀ ⦃U : set α⦄, U ∈ g → U ∈ f, lt := preorder.lt._default (λ (f g : filter α), ∀ ⦃U : set α⦄, U ∈ g → U ∈ f), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

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

set (set α) → set α → Prop

basic : ∀ {α : Type u} (g : set (set α)) {s : set α}, s ∈ g → filter.generate_sets g s
univ : ∀ {α : Type u} (g : set (set α)), filter.generate_sets g set.univ
superset : ∀ {α : Type u} (g : set (set α)) {s t : set α}, filter.generate_sets g s → s ⊆ t → filter.generate_sets g t
inter : ∀ {α : Type u} (g : set (set α)) {s t : set α}, filter.generate_sets g s → filter.generate_sets g t → filter.generate_sets g (s ∩ t)

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

source

def filter.generate {α : Type u} :

set (set α) → filter α

generate g is the smallest filter containing the sets g.

Equations

filter.generate g = {sets := filter.generate_sets g, univ_sets := _, sets_of_superset := _, inter_sets := _}

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

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

(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

filter.mk_of_closure s hs = {sets := s, univ_sets := _, sets_of_superset := _, inter_sets := _}

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

filter.gi_generate α = {choice := λ (s : set (set α)) (hs : (filter.generate s).sets ≤ s), filter.mk_of_closure s _, gc := _, le_l_u := _, choice_eq := _}

source

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

filter.has_inf = {inf := λ (f g : filter α), {sets := {s : set α | ∃ (a : set α) (H : a ∈ f) (b : set α) (H : b ∈ g), a ∩ b ⊆ s}, univ_sets := _, sets_of_superset := _, inter_sets := _}}

source

@[simp]

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

s ∈ f ⊓ g ↔ ∃ (t₁ : set α) (H : t₁ ∈ f) (t₂ : set α) (H : t₂ ∈ g), t₁ ∩ t₂ ⊆ s

source

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

s ∈ f → s ∈ f ⊓ g

source

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

s ∈ g → s ∈ f ⊓ g

source

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

s ∈ f → t ∈ g → s ∩ t ∈ f ⊓ g

source

@[instance]

def filter.has_top {α : Type u} :

has_top (filter α)

Equations

filter.has_top = {top := {sets := {s : set α | ∀ (x : α), x ∈ s}, univ_sets := _, sets_of_superset := _, inter_sets := _}}

source

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

s ∈ ⊤ ↔ ∀ (x : α), x ∈ s

source

@[simp]

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

s ∈ ⊤ ↔ s = set.univ

source

@[instance]

def filter.complete_lattice {α : Type u} :

complete_lattice (filter α)

Equations

filter.complete_lattice = original_complete_lattice.copy partial_order.le filter.complete_lattice._proof_1 ⊤ filter.complete_lattice._proof_2 complete_lattice.bot filter.complete_lattice._proof_3 complete_lattice.sup filter.complete_lattice._proof_4 has_inf.inf filter.complete_lattice._proof_5 (filter.join ∘ filter.principal) filter.complete_lattice._proof_6 complete_lattice.Inf filter.complete_lattice._proof_7

source

@[class]

def filter.ne_bot {α : Type u} :

filter α → Prop

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

Equations

f.ne_bot = (f ≠ ⊥)

Instances

source

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

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

f.ne_bot → f ≤ g → g.ne_bot

source

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

f ≤ g → 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 α)} :

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

s ∈ ⊥

source

@[simp]

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

s ∈ f → t ∈ g → s ∪ t ∈ f ⊔ g

source

@[simp]

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

x ∈ has_Sup.Sup s ↔ ∀ (f : filter α), f ∈ s → x ∈ f

source

@[simp]

theorem filter.mem_supr_sets {α : Type u} {ι : Sort x} {x : set α} {f : ι → filter α} :

x ∈ supr f ↔ ∀ (i : ι), x ∈ f i

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_iff {α : Type u} {ι : Type u_1} {s : ι → filter α} {U : set α} :

(U ∈ ⨅ (i : ι), s i) ↔ ∃ (I : set ι), I.finite ∧ ∃ (V : ↥{i : ι | i ∈ I} → set α), (∀ (i : ↥{i : ι | i ∈ I}), V i ∈ s ↑i) ∧ (⋂ (i : ↥{i : ι | i ∈ I}), V i) ⊆ U

source

@[simp]

theorem filter.le_principal_iff {α : Type u} {s : set α} {f : filter α} :

f ≤ filter.principal s ↔ s ∈ f

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.empty_in_sets_eq_bot {α : Type u} {f : filter α} :

∅ ∈ f ↔ f = ⊥

source

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

s ∈ f → s.nonempty

source

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

s ∈ f → s.nonempty

source

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

nonempty α

source

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

¬nonempty α → f = ⊥

source

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

(∀ (s : set α), s ∈ f → s.nonempty) ↔ f.ne_bot

source

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

f ⊓ filter.principal sᶜ = ⊥ → s ∈ f

source

theorem filter.inf_ne_bot_iff {α : Type u} {f g : filter α} :

(f ⊓ g).ne_bot ↔ ∀ {U V : set α}, U ∈ f → V ∈ g → (U ∩ V).nonempty

source

theorem filter.inf_principal_ne_bot_iff {α : Type u} {f : filter α} {s : set α} :

(f ⊓ filter.principal s).ne_bot ↔ ∀ (U : set α), U ∈ f → (U ∩ s).nonempty

source

theorem filter.inf_eq_bot_iff {α : Type u} {f g : filter α} :

f ⊓ g = ⊥ ↔ ∃ (U V : set α), U ∈ f ∧ V ∈ g ∧ U ∩ V = ∅

source

theorem filter.disjoint_iff {α : Type u} {f g : filter α} :

disjoint f g ↔ ∃ (U V : set α), U ∈ f ∧ V ∈ g ∧ U ∩ V = ∅

source

theorem filter.eq_Inf_of_mem_sets_iff_exists_mem {α : Type u} {S : set (filter α)} {l : filter α} :

(∀ {s : set α}, s ∈ l ↔ ∃ (f : filter α) (H : f ∈ S), s ∈ f) → l = has_Inf.Inf S

source

theorem filter.eq_infi_of_mem_sets_iff_exists_mem {α : Type u} {ι : Sort x} {f : ι → filter α} {l : filter α} :

(∀ {s : set α}, s ∈ l ↔ ∃ (i : ι), s ∈ f i) → l = infi f

source

theorem filter.eq_binfi_of_mem_sets_iff_exists_mem {α : Type u} {ι : Sort x} {f : ι → filter α} {p : ι → Prop} {l : filter α} :

(∀ {s : set α}, s ∈ l ↔ ∃ (i : ι) (_x : p i), s ∈ f i) → (l = ⨅ (i : ι) (_x : p i), f i)

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 {α : Type u} {ι : Sort x} {f : ι → filter α} (h : directed ge f) [nonempty ι] (s : set α) :

s ∈ infi f ↔ ∃ (i : ι), s ∈ f i

source

theorem filter.binfi_sets_eq {α : Type u} {β : Type v} {f : β → filter α} {s : set β} :

directed_on (f ⁻¹'o ge) s → s.nonempty → ((⨅ (i : β) (H : i ∈ s), f i).sets = ⋃ (i : β) (H : i ∈ s), (f i).sets)

source

theorem filter.mem_binfi {α : Type u} {β : Type v} {f : β → filter α} {s : set β} (h : directed_on (f ⁻¹'o ge) s) (ne : s.nonempty) {t : set α} :

(t ∈ ⨅ (i : β) (H : i ∈ s), f i) ↔ ∃ (i : β) (H : i ∈ s), t ∈ f i

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 ↔ s ∈ ⋃ (t : finset ι), (⨅ (i : ι) (H : i ∈ t), f i).sets

source

theorem filter.mem_infi_finite' {α : Type u} {ι : Sort x} {f : ι → filter α} (s : set α) :

s ∈ infi f ↔ s ∈ ⋃ (t : finset (plift ι)), (⨅ (i : plift ι) (H : i ∈ t), f i.down).sets

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

@[instance]

def filter.bounded_distrib_lattice {α : Type u} :

bounded_distrib_lattice (filter α)

Equations

filter.bounded_distrib_lattice = {sup := complete_lattice.sup filter.complete_lattice, le := complete_lattice.le filter.complete_lattice, lt := complete_lattice.lt filter.complete_lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := complete_lattice.inf filter.complete_lattice, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _, top := complete_lattice.top filter.complete_lattice, le_top := _, bot := complete_lattice.bot filter.complete_lattice, bot_le := _}

source

theorem filter.infi_sup_left {α : Type u} {ι : Sort x} {f : filter α} {g : ι → filter α} :

(⨅ (x : ι), f ⊔ g x) = f ⊔ infi g

source

theorem filter.infi_sup_right {α : Type u} {ι : Sort x} {f : filter α} {g : ι → filter α} :

(⨅ (x : ι), g x ⊔ f) = infi g ⊔ f

source

theorem filter.binfi_sup_right {α : Type u} {ι : Sort x} (p : ι → Prop) (f : ι → filter α) (g : filter α) :

(⨅ (i : ι) (h : p i), f i ⊔ g) = (⨅ (i : ι) (h : p i), f i) ⊔ g

source

theorem filter.binfi_sup_left {α : Type u} {ι : Sort x} (p : ι → Prop) (f : ι → filter α) (g : filter α) :

(⨅ (i : ι) (h : p i), g ⊔ f i) = g ⊔ ⨅ (i : ι) (h : p i), f i

source

theorem filter.mem_infi_sets_finset {α : Type u} {β : Type v} {s : finset α} {f : α → filter β} (t : set β) :

(t ∈ ⨅ (a : α) (H : a ∈ s), f a) ↔ ∃ (p : α → set β), (∀ (a : α), a ∈ s → p a ∈ f a) ∧ (⋂ (a : α) (H : a ∈ s), p a) ⊆ t

source

theorem filter.infi_ne_bot_of_directed' {α : Type u} {ι : Sort x} {f : ι → filter α} [nonempty ι] :

directed ge f → (∀ (i : ι), (f i).ne_bot) → (infi f).ne_bot

If f : ι → filter α is directed, ι is not empty, and ∀ i, f i ≠ ⊥, then infi f ≠ ⊥. See also infi_ne_bot_of_directed for a version assuming nonempty α instead of nonempty ι.

source

theorem filter.infi_ne_bot_of_directed {α : Type u} {ι : Sort x} {f : ι → filter α} [hn : nonempty α] :

directed ge f → (∀ (i : ι), (f i).ne_bot) → (infi f).ne_bot

If f : ι → filter α is directed, α is not empty, and ∀ i, f i ≠ ⊥, then infi f ≠ ⊥. See also infi_ne_bot_of_directed' for a version assuming nonempty ι instead of nonempty α.

source

theorem filter.infi_ne_bot_iff_of_directed' {α : Type u} {ι : Sort x} {f : ι → filter α} [nonempty ι] :

directed ge f → ((infi f).ne_bot ↔ ∀ (i : ι), (f i).ne_bot)

source

theorem filter.infi_ne_bot_iff_of_directed {α : Type u} {ι : Sort x} {f : ι → filter α} [nonempty α] :

directed ge f → ((infi f).ne_bot ↔ ∀ (i : ι), (f i).ne_bot)

source

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

s ∈ f i → (s ∈ ⨅ (i : ι), f i)

source

theorem filter.infi_sets_induct {α : Type u} {ι : Sort x} {f : ι → filter α} {s : set α} (hs : s ∈ infi f) {p : set α → Prop} :

p set.univ → (∀ {i : ι} {s₁ s₂ : set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)) → (∀ {s₁ s₂ : set α}, s₁ ⊆ s₂ → p s₁ → p s₂) → p s

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

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

(filter.principal s).ne_bot ↔ s.nonempty

source

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

is_compl (filter.principal s) (filter.principal sᶜ)

source

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

sᶜ ∈ f → f ⊓ filter.principal s = ⊥

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.mem_iff_inf_principal_compl {α : Type u} {f : filter α} {V : set α} :

V ∈ f ↔ f ⊓ filter.principal Vᶜ = ⊥

source

theorem filter.le_iff_forall_inf_principal_compl {α : Type u} {f g : filter α} :

f ≤ g ↔ ∀ (V : set α), V ∈ g → f ⊓ filter.principal Vᶜ = ⊥

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_fintype {α : Type u} {ι : Type w} [fintype ι] (f : ι → set α) :

(⨅ (i : ι), filter.principal (f i)) = filter.principal (⋂ (i : ι), f i)

source

theorem filter.join_mono {α : Type u} {f₁ f₂ : filter (filter α)} :

f₁ ≤ f₂ → f₁.join ≤ f₂.join

source

def filter.eventually {α : Type u} :

(α → Prop) → filter α → Prop

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

Equations

filter.eventually p f = ({x : α | p x} ∈ f)

source

theorem filter.eventually_iff {α : Type u} {f : filter α} {P : α → Prop} :

(∀ᶠ (x : α) in f, P x) ↔ {x : α | P x} ∈ f

source

theorem filter.ext' {α : Type u} {f₁ f₂ : filter α} :

(∀ (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} :

(∀ᶠ (x : α) in f₂, p x) → (∀ᶠ (x : α) in f₁, p x)

source

theorem filter.eventually_of_mem {α : Type u} {f : filter α} {P : α → Prop} {U : set α} :

U ∈ f → (∀ (x : α), x ∈ U → P x) → (∀ᶠ (x : α) in f, P x)

source

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

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

(∀ᶠ (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 α} :

(∀ᶠ (x : α) in f, p x) → (∀ᶠ (x : α) in f, p x → q x) → (∀ᶠ (x : α) in f, q x)

source

theorem filter.eventually.mono {α : Type u} {p q : α → Prop} {f : filter α} :

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

(∀ᶠ (x : α) in f, p x) → (∀ᶠ (x : α) in f, p x ↔ q x) → (∀ᶠ (x : α) in f, q x)

source

theorem filter.eventually_congr {α : Type u} {f : filter α} {p q : α → Prop} :

(∀ᶠ (x : α) in f, p x ↔ q x) → ((∀ᶠ (x : α) in f, p x) ↔ ∀ᶠ (x : α) in f, q x)

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

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} {β : 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 filter.principal a, p x) ↔ ∀ (x : α), x ∈ a → 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

source

def filter.frequently {α : Type u} :

(α → Prop) → filter α → Prop

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

Equations

filter.frequently p f = ¬∀ᶠ (x : α) in f, ¬p x

source

theorem filter.eventually.frequently {α : Type u} {f : filter α} [f.ne_bot] {p : α → Prop} :

(∀ᶠ (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} :

(∀ (x : α), p x) → (∃ᶠ (x : α) in f, p x)

source

theorem filter.frequently.mp {α : Type u} {p q : α → Prop} {f : filter α} :

(∃ᶠ (x : α) in f, p x) → (∀ᶠ (x : α) in f, p x → q x) → (∃ᶠ (x : α) in f, q x)

source

theorem filter.frequently.mono {α : Type u} {p q : α → Prop} {f : filter α} :

(∃ᶠ (x : α) in f, p x) → (∀ (x : α), p x → q x) → (∃ᶠ (x : α) in f, q x)

source

theorem filter.frequently.and_eventually {α : Type u} {p q : α → Prop} {f : filter α} :

(∃ᶠ (x : α) in f, p x) → (∀ᶠ (x : α) in f, q x) → (∃ᶠ (x : α) in f, p x ∧ q x)

source

theorem filter.frequently.exists {α : Type u} {p : α → Prop} {f : filter α} :

(∃ᶠ (x : α) in f, p x) → (∃ (x : α), p x)

source

theorem filter.eventually.exists {α : Type u} {p : α → Prop} {f : filter α} [f.ne_bot] :

(∀ᶠ (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_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

theorem filter.inf_ne_bot_iff_frequently_left {α : Type u} {f g : filter α} :

(f ⊓ g).ne_bot ↔ ∀ {p : α → Prop}, (∀ᶠ (x : α) in f, p x) → (∃ᶠ (x : α) in g, p x)

source

theorem filter.inf_ne_bot_iff_frequently_right {α : Type u} {f g : filter α} :

(f ⊓ g).ne_bot ↔ ∀ {p : α → Prop}, (∀ᶠ (x : α) in g, p x) → (∃ᶠ (x : α) in f, p x)

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

def filter.eventually_eq {α : Type u} {β : Type v} :

filter α → (α → β) → (α → β) → Prop

Two functions f and g are eventually equal along a filter l if the set of x such that f x = g x belongs to l.

Equations

f =ᶠ[l] g = ∀ᶠ (x : α) in l, f x = g x

source

theorem filter.eventually_eq.eventually {α : Type u} {β : Type v} {l : filter α} {f g : α → β} :

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

(∀ᶠ (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_eq.exists_mem {α : Type u} {β : Type v} {l : filter α} {f g : α → β} :

f =ᶠ[l] g → (∃ (s : set α) (H : s ∈ l), set.eq_on f g s)

source

theorem filter.eventually_eq_of_mem {α : Type u} {β : Type v} {l : filter α} {f g : α → β} {s : set α} :

s ∈ l → 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 : α → β} :

f =ᶠ[l] g → 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.symm {α : Type u} {β : Type v} {f g : α → β} {l : filter α} :

f =ᶠ[l] g → g =ᶠ[l] f

source

theorem filter.eventually_eq.trans {α : Type u} {β : Type v} {f g h : α → β} {l : filter α} :

f =ᶠ[l] g → 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' : α → γ} :

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 : β → γ → δ) :

g =ᶠ[l] g' → ((λ (x : α), h (f x) (g x)) =ᶠ[l] λ (x : α), h (f' x) (g' x))

source

theorem filter.eventually_eq.mul {α : Type u} {β : Type v} [has_mul β] {f f' g g' : α → β} {l : filter α} :

f =ᶠ[l] g → f' =ᶠ[l] g' → ((λ (x : α), f x * f' x) =ᶠ[l] λ (x : α), g x * g' x)

source

theorem filter.eventually_eq.add {α : Type u} {β : Type v} [has_add β] {f f' g g' : α → β} {l : filter α} :

f =ᶠ[l] g → 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 α} :

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

f =ᶠ[l] g → ((λ (x : α), (f x)⁻¹) =ᶠ[l] λ (x : α), (g x)⁻¹)

source

theorem filter.eventually_eq.div {α : Type u} {β : Type v} [group_with_zero β] {f f' g g' : α → β} {l : filter α} :

f =ᶠ[l] g → f' =ᶠ[l] g' → ((λ (x : α), f x / f' x) =ᶠ[l] λ (x : α), g x / g' x)

source

theorem filter.eventually_eq.sub {α : Type u} {β : Type v} [add_group β] {f f' g g' : α → β} {l : filter α} :

f =ᶠ[l] g → f' =ᶠ[l] g' → ((λ (x : α), f x - f' x) =ᶠ[l] λ (x : α), g x - g' x)

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

def filter.eventually_le {α : Type u} {β : Type v} [has_le β] :

filter α → (α → β) → (α → β) → Prop

A function f is eventually less than or equal to a function g at a filter l.

Equations

f ≤ᶠ[l] g = ∀ᶠ (x : α) in l, f x ≤ g x

source

theorem filter.eventually_le.congr {α : Type u} {β : Type v} [has_le β] {l : filter α} {f f' g g' : α → β} :

f ≤ᶠ[l] g → f =ᶠ[l] f' → g =ᶠ[l] g' → f' ≤ᶠ[l] g'

source

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

f =ᶠ[l] f' → g =ᶠ[l] g' → (f ≤ᶠ[l] g ↔ f' ≤ᶠ[l] g')

source

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

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.trans {α : Type u} {β : Type v} [preorder β] {l : filter α} {f g h : α → β} :

f ≤ᶠ[l] g → g ≤ᶠ[l] h → f ≤ᶠ[l] h

source

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

f =ᶠ[l] g → g ≤ᶠ[l] h → f ≤ᶠ[l] h

source

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

f ≤ᶠ[l] g → g =ᶠ[l] h → f ≤ᶠ[l] h

source

theorem filter.eventually_le.antisymm {α : Type u} {β : Type v} [partial_order β] {l : filter α} {f g : α → β} :

f ≤ᶠ[l] g → g ≤ᶠ[l] f → f =ᶠ[l] g

source

theorem filter.join_le {α : Type u} {f : filter (filter α)} {l : filter α} :

(∀ᶠ (m : filter α) in f, m ≤ l) → f.join ≤ l

source

def filter.map {α : Type u} {β : Type v} :

(α → β) → filter α → filter β

The forward map of a filter

Equations

filter.map m f = {sets := set.preimage m ⁻¹' f.sets, univ_sets := _, sets_of_superset := _, inter_sets := _}

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 ↔ {x : α | m x ∈ t} ∈ f

source

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

s ∈ f → m '' s ∈ filter.map m 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_sets_iff {α : 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_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 α} :

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

(α → β) → filter β → filter α

The inverse map of a filter

Equations

filter.comap m f = {sets := {s : set α | ∃ (t : set β) (H : t ∈ f), m ⁻¹' t ⊆ s}, univ_sets := _, sets_of_superset := _, inter_sets := _}

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

filter α → (α → filter β) → filter β

The monadic bind operation on filter is defined the usual way in terms of map and join.

Unfortunately, this bind does not result in the expected applicative. See filter.seq for the applicative instance.

Equations

f.bind m = (filter.map m f).join

source

def filter.seq {α : Type u} {β : Type v} :

filter (α → β) → filter α → filter β

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

Equations

f.seq g = {sets := {s : set β | ∃ (u : set (α → β)) (H : u ∈ f) (t : set α) (H : t ∈ g), ∀ (m : α → β), m ∈ u → ∀ (x : α), x ∈ t → m x ∈ s}, univ_sets := _, sets_of_superset := _, inter_sets := _}

source

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

filter.has_pure = {pure := λ (α : Type u) (x : α), {sets := {s : set α | x ∈ s}, univ_sets := trivial, sets_of_superset := _, inter_sets := _}}

source

@[instance]

def filter.has_bind :

has_bind filter

Equations

filter.has_bind = {bind := filter.bind}

source

@[instance]

def filter.has_seq :

has_seq filter

Equations

filter.has_seq = {seq := filter.seq}

source

@[instance]

def filter.functor :

functor filter

Equations

filter.functor = {map := filter.map, map_const := λ (α β : Type u_1), filter.map ∘ function.const β}

source

theorem filter.pure_sets {α : Type u} (a : α) :

(has_pure.pure a).sets = {s : set α | a ∈ s}

source

@[simp]

theorem filter.mem_pure_sets {α : 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

def filter.monad :

monad filter

The monad structure on filters.

Equations

filter.monad = monad.mk

source

theorem filter.is_lawful_monad :

is_lawful_monad filter

source

@[instance]

def filter.applicative :

applicative filter

Equations

filter.applicative = applicative.mk

source

@[instance]

def filter.alternative :

alternative filter

Equations

filter.alternative = {to_applicative := {to_functor := {map := λ (_x _x_1 : Type u_1) (x : _x → _x_1) (y : filter _x), has_pure.pure x <*> y, map_const := λ (α β : Type u_1), (λ (x : β → α) (y : filter β), has_pure.pure x <*> y) ∘ function.const β}, to_has_pure := filter.has_pure, to_has_seq := filter.has_seq, to_has_seq_left := {seq_left := λ (α β : Type u_1) (a : filter α) (b : filter β), (λ (_x _x_1 : Type u_1) (x : _x → _x_1) (y : filter _x), has_pure.pure x <*> y) α (β → α) (function.const β) a <*> b}, to_has_seq_right := {seq_right := λ (α β : Type u_1) (a : filter α) (b : filter β), (λ (_x _x_1 : Type u_1) (x : _x → _x_1) (y : filter _x), has_pure.pure x <*> y) α (β → β) (function.const α id) a <*> b}}, to_has_orelse := {orelse := λ (α : Type u_1) (x y : filter α), x ⊔ y}, failure := λ (α : Type u_1), ⊥}

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

source

@[simp]

theorem filter.mem_comap_sets {α : Type u} {β : Type v} {g : filter β} {m : α → β} {s : set α} :

s ∈ filter.comap m g ↔ ∃ (t : set β) (H : t ∈ g), m ⁻¹' t ⊆ s

source

theorem filter.preimage_mem_comap {α : Type u} {β : Type v} {g : filter β} {m : α → β} {t : set β} :

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} {x : α} {f : filter α} {V : set α} :

V ∈ f → x ∉ V → filter.comap (λ (y : α), x) f = ⊥

source

theorem filter.comap_const_of_mem {α : Type u} {x : α} {f : filter α} :

(∀ (V : set α), V ∈ f → x ∈ V) → filter.comap (λ (y : α), x) f = ⊤

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

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

set.range m ∈ f → filter.map m (filter.comap m f) = f

source

theorem filter.image_mem_sets {α : Type u} {β : Type v} {f : filter α} {c : β → α} (h : set.range c ∈ f) {W : set β} :

W ∈ filter.comap c f → c '' W ∈ f

source

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

W ∈ filter.comap coe f → coe '' W ∈ f

source

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

(∀ (x y : α), m x = m y → x = y) → filter.comap m (filter.map m f) = f

source

theorem filter.le_of_map_le_map_inj' {α : Type u} {β : Type v} {f g : filter α} {m : α → β} {s : set α} :

s ∈ f → s ∈ g → (∀ (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.le_of_map_le_map_inj_iff {α : Type u} {β : Type v} {f g : filter α} {m : α → β} {s : set α} :

s ∈ f → s ∈ g → (∀ (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 α} :

s ∈ f → s ∈ g → (∀ (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.map_inj {α : Type u} {β : Type v} {f g : filter α} {m : α → β} :

(∀ (x y : α), m x = m y → x = y) → filter.map m f = filter.map m g → f = g

source

theorem filter.le_map_comap_of_surjective' {α : Type u} {β : Type v} {f : α → β} {l : filter β} {u : set β} :

u ∈ l → (∀ (y : β), y ∈ u → (∃ (x : α), f x = y)) → l ≤ filter.map f (filter.comap f l)

source

theorem filter.map_comap_of_surjective' {α : Type u} {β : Type v} {f : α → β} {l : filter β} {u : set β} :

u ∈ l → (∀ (y : β), y ∈ u → (∃ (x : α), f x = y)) → filter.map f (filter.comap f l) = l

source

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

l ≤ filter.map f (filter.comap f l)

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 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.subtype_coe_map_comap_prod {α : Type u} (s : set α) (f : filter (α × α)) :

filter.map coe (filter.comap coe f) = f ⊓ filter.principal (s.prod s)

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

(∀ (t : set β), t ∈ f → (∃ (a : α), m a ∈ t)) → (filter.comap m f).ne_bot

source

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

f.ne_bot → set.range m ∈ f → (filter.comap m 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 α} :

m '' s ∈ f → (filter.comap m f ⊓ filter.principal s).ne_bot

source

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

f.ne_bot → 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 α} :

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

@[instance]

def filter.map_ne_bot {α : Type u} {β : Type v} {f : filter α} {m : α → β} [hf : f.ne_bot] :

(filter.map m f).ne_bot

Equations

filter.map_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} :

directed_on (f ⁻¹'o ge) {x : ι | p x} → (∃ (i : ι), p i) → (filter.map m (⨅ (i : ι) (h : p i), f i) = ⨅ (i : ι) (h : p i), filter.map m (f i))

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 : α → β} {t : set α} :

t ∈ f → t ∈ g → (∀ (x : α), x ∈ t → ∀ (y : α), y ∈ t → m x = m y → x = y) → 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 : α → β} :

function.injective m → filter.map m (f ⊓ g) = filter.map m f ⊓ filter.map m g

source

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

m ∘ n = id → n ∘ m = id → filter.map m f = filter.comap n 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 β} :

(∀ (s : set α), s ∈ f → m '' s ∈ g) → g ≤ filter.map m f

source

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

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

{a} ∈ has_pure.pure a

source

theorem filter.pure_injective {α : Type u} :

function.injective has_pure.pure

source

@[instance]

def filter.pure_ne_bot {α : Type u} {a : α} :

(has_pure.pure a).ne_bot

Equations

filter.pure_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_sets_def {α : Type u} {β : Type v} {f : filter (α → β)} {g : filter α} {s : set β} :

s ∈ f.seq g ↔ ∃ (u : set (α → β)) (H : u ∈ f) (t : set α) (H : t ∈ g), ∀ (x : α → β), x ∈ u → ∀ (y : α), y ∈ t → x y ∈ s

source

theorem filter.mem_seq_sets_iff {α : Type u} {β : Type v} {f : filter (α → β)} {g : filter α} {s : set β} :

s ∈ f.seq g ↔ ∃ (u : set (α → β)) (H : u ∈ f) (t : set α) (H : t ∈ g), u.seq t ⊆ s

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

s ∈ f → t ∈ g → s.seq t ∈ f.seq g

source

theorem filter.le_seq {α : Type u} {β : Type v} {f : filter (α → β)} {g : filter α} {h : filter β} :

(∀ (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 α} :

f₁ ≤ f₂ → 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

@[instance]

def filter.is_lawful_functor :

is_lawful_functor filter

Equations

filter.is_lawful_functor = _

source

@[instance]

def filter.is_lawful_applicative :

is_lawful_applicative filter

Equations

filter.is_lawful_applicative = _

source

@[instance]

def filter.is_comm_applicative :

is_comm_applicative filter

Equations

filter.is_comm_applicative = _

source

theorem filter.seq_eq_filter_seq {α β : Type l} (f : filter (α → β)) (g : filter α) :

f <*> g = f.seq g

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_sets' {α : 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_sets {α : 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 β} :

(∀ᶠ (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 β} :

f₁ ≤ f₂ → 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_sets {α' β' γ' : 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_sets_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

source

def filter.tendsto {α : Type u} {β : Type v} :

(α → β) → filter α → filter β → Prop

tendsto is the generic "limit of a function" predicate. tendsto f l₁ l₂ asserts that for every l₂ neighborhood a, the f-preimage of a is an l₁ neighborhood.

Equations

filter.tendsto f l₁ l₂ = (filter.map f l₁ ≤ l₂)

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

filter.tendsto f l₁ l₂ → (∀ᶠ (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} :

filter.tendsto f l₁ l₂ → (∃ᶠ (x : α) in l₁, p (f x)) → (∃ᶠ (y : β) in l₂, p y)

source

@[simp]

theorem filter.tendsto_bot {α : Type u} {β : Type v} {f : α → β} {l : filter β} :

filter.tendsto f ⊥ l

source

theorem filter.tendsto_of_not_nonempty {α : Type u} {β : Type v} {f : α → β} {la : filter α} {lb : filter β} :

¬nonempty α → 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 β} :

(∀ᶠ (x : α) in fa, g₁ (f x) = x) → (∀ᶠ (y : β) in fb, f (g₂ y) = y) → 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_congr' {α : Type u} {β : Type v} {f₁ f₂ : α → β} {l₁ : filter α} {l₂ : filter β} :

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

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

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

(∀ (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 γ} :

filter.tendsto g y z → 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 β} :

filter.tendsto f x z → y ≤ x → filter.tendsto f y z

source

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

filter.tendsto f x y → 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 γ} :

filter.tendsto (f ∘ g) x y → filter.tendsto f (filter.map g x) y

source

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

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

set.range i ∈ f → (filter.tendsto (m ∘ i) (filter.comap i f) g ↔ filter.tendsto m f g)

source

theorem filter.comap_eq_of_inverse {α : Type u} {β : Type v} {f : filter α} {g : filter β} {φ : α → β} (ψ : β → α) :

ψ ∘ φ = id → filter.tendsto φ f g → filter.tendsto ψ g f → filter.comap φ g = f

source

theorem filter.map_eq_of_inverse {α : Type u} {β : Type v} {f : filter α} {g : filter β} {φ : α → β} (ψ : β → α) :

φ ∘ ψ = id → filter.tendsto φ f g → 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 β} :

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

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

filter.tendsto f x₁ y₁ → 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 : ι) :

filter.tendsto f (x i) y → filter.tendsto f (⨅ (i : ι), x i) y

source

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

theorem filter.tendsto.not_tendsto {α : Type u} {β : Type v} {f : α → β} {a : filter α} {b₁ b₂ : filter β} (hf : filter.tendsto f a b₁) [a.ne_bot] :

disjoint b₁ b₂ → ¬filter.tendsto f a b₂

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

source

theorem filter.tendsto_if {α : Type u} {β : Type v} {l₁ : filter α} {l₂ : filter β} {f g : α → β} {p : α → Prop} [decidable_pred p] :

filter.tendsto f (l₁ ⊓ filter.principal p) l₂ → filter.tendsto g (l₁ ⊓ filter.principal {x : α | ¬p x}) l₂ → filter.tendsto (λ (x : α), ite (p x) (f x) (g x)) l₁ l₂

source

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

filter α → filter β → filter (α × β)

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

Equations

f.prod g = filter.comap prod.fst f ⊓ filter.comap prod.snd g

source

theorem filter.prod_mem_prod {α : Type u} {β : Type v} {s : set α} {t : set β} {f : filter α} {g : filter β} :

s ∈ f → t ∈ g → s.prod t ∈ f.prod g

source

theorem filter.mem_prod_iff {α : Type u} {β : Type v} {s : set (α × β)} {f : filter α} {g : filter β} :

s ∈ f.prod g ↔ ∃ (t₁ : set α) (H : t₁ ∈ f) (t₂ : set β) (H : t₂ ∈ g), t₁.prod t₂ ⊆ s

source

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

filter.comap f (b.prod c) = filter.comap (prod.fst ∘ f) b ⊓ filter.comap (prod.snd ∘ f) c

source

theorem filter.eventually_prod_iff {α : Type u} {β : Type v} {p : α × β → Prop} {f : filter α} {g : filter β} :

(∀ᶠ (x : α × β) in f.prod 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.prod g) f

source

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

filter.tendsto prod.snd (f.prod g) g

source

theorem filter.tendsto.prod_mk {α : Type u} {β : Type v} {γ : Type w} {f : filter α} {g : filter β} {h : filter γ} {m₁ : α → β} {m₂ : α → γ} :

filter.tendsto m₁ f g → filter.tendsto m₂ f h → filter.tendsto (λ (x : α), (m₁ x, m₂ x)) f (g.prod 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.prod 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.prod 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} :

(∀ᶠ (y : β) in lb, pb y) → (∀ᶠ (p : α × β) in la.prod lb, pa p.fst ∧ pb p.snd)

source

theorem filter.eventually.curry {α : Type u} {β : Type v} {la : filter α} {lb : filter β} {p : α × β → Prop} :

(∀ᶠ (x : α × β) in la.prod 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).prod g = ⨅ (i : ι), (f i).prod g

source

theorem filter.prod_infi_right {α : Type u} {β : Type v} {ι : Sort x} [nonempty ι] {f : filter α} {g : ι → filter β} :

f.prod (⨅ (i : ι), g i) = ⨅ (i : ι), f.prod (g i)

source

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

f₁ ≤ f₂ → g₁ ≤ g₂ → f₁.prod g₁ ≤ f₂.prod 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₁).prod (filter.comap m₂ f₂) = filter.comap (λ (p : β₁ × β₂), (m₁ p.fst, m₂ p.snd)) (f₁.prod f₂)

source

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

f.prod g = filter.comap prod.swap (g.prod f)

source

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

f.prod g = filter.map (λ (p : β × α), (p.snd, p.fst)) (g.prod 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₁).prod (filter.map m₂ f₂) = filter.map (λ (p : α₁ × α₂), (m₁ p.fst, m₂ p.snd)) (f₁.prod 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 δ} :

filter.tendsto f a c → filter.tendsto g b d → filter.tendsto (prod.map f g) (a.prod b) (c.prod d)

source

theorem filter.map_prod {α : Type u} {β : Type v} {γ : Type w} (m : α × β → γ) (f : filter α) (g : filter β) :

filter.map m (f.prod 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.prod 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₁.prod g₁ ⊓ f₂.prod g₂ = (f₁ ⊓ f₂).prod (g₁ ⊓ g₂)

source

@[simp]

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

f.prod ⊥ = ⊥

source

@[simp]

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

⊥.prod g = ⊥

source

@[simp]

theorem filter.prod_principal_principal {α : Type u} {β : Type v} {s : set α} {t : set β} :

(filter.principal s).prod (filter.principal t) = filter.principal (s.prod t)

source

@[simp]

theorem filter.prod_pure_pure {α : Type u} {β : Type v} {a : α} {b : β} :

(has_pure.pure a).prod (has_pure.pure b) = has_pure.pure (a, b)

source

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

f.prod g = ⊥ ↔ f = ⊥ ∨ g = ⊥

source

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

(f.prod g).ne_bot ↔ f.ne_bot ∧ g.ne_bot

source

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

f.ne_bot → g.ne_bot → (f.prod g).ne_bot

source

@[instance]

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

(f.prod g).ne_bot

Equations

filter.prod_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.prod 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 set.eq_on.eventually_eq {α : Type u_1} {β : Type u_2} {s : set α} {f g : α → β} :

set.eq_on f g s → f =ᶠ[filter.principal s] g

mathlib documentation

order.filter.basic

Theory of filters on sets

Main definitions

Notations

References

Lattice equations

Eventually

Frequently

Relation “eventually equal”

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

Limits

Products of filters

General documentation

Additional documentation

Library

mathlib documentation

order.​filter.​basic

Theory of filters on sets

Main definitions

Notations

References

Lattice equations

Eventually

Frequently

Relation “eventually equal”

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

Limits

Products of filters

General documentation

Additional documentation

Library

order.filter.basic