Theory of filters on sets

Main definitions

• Filter : filters on a set;
• Filter.principal : filter of all sets containing a given set;
• Filter.map, Filter.comap : operations on filters;
• Filter.Tendsto : limit with respect to filters;
• Filter.Eventually : f.eventually p means {x | p x} ∈ f;
• Filter.Frequently : f.frequently p means {x | ¬p x} ∉ f;
• filter_upwards [h₁, ..., hₙ] : a tactic that takes a list of proofs hᵢ : sᵢ ∈ f, and replaces a goal s ∈ f with ∀ x, x ∈ s₁ → ... → x ∈ sₙ → x ∈ s;
• Filter.NeBot f : a utility class stating that f is a non-trivial filter.

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:

• limits, including finite or infinite limits of sequences, finite or infinite limits of functions at a point or at infinity, etc...
• things happening eventually, including things happening for large enough n : ℕ, or near enough a point x, or for close enough pairs of points, or things happening almost everywhere in the sense of measure theory. Dually, filters can also express the idea of things happening often: for arbitrarily large n, or at a point in any neighborhood of given a point etc...

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:

• (Filter.atTop : Filter ℕ) : made of sets of ℕ containing {n | n ≥ N} for some N
• 𝓝 x : made of neighborhoods of x in a topological space (defined in topology.basic)
• 𝓤 X : made of entourages of a uniform space (those space are generalizations of metric spaces defined in Mathlib/Topology/UniformSpace/Basic.lean)
• MeasureTheory.ae : made of sets whose complement has zero measure with respect to μ (defined in Mathlib/MeasureTheory/OuterMeasure/AE)

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 atTop (𝓝 x) → (∀ᶠ n in atTop, u n ∈ M) → x ∈ closure M, which is a special case of mem_closure_of_tendsto from Topology.Basic.

Notations

• ∀ᶠ x in f, p x : f.Eventually p;
• ∃ᶠ x in f, p x : f.Frequently p;
• f =ᶠ[l] g : ∀ᶠ x in l, f x = g x;
• f ≤ᶠ[l] g : ∀ᶠ x in l, f x ≤ g x;
• 𝓟 s : Filter.Principal s, localized in Filter.

References

• [N. Bourbaki, General Topology][bourbaki1966]

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 [NeBot f] in a number of lemmas and definitions.

structure Filter (α : Type u_1) : Type u_1

A filter F on a type α is a collection of sets of α which contains the whole α, is upwards-closed, and is stable under intersection. We do not forbid this collection to be all sets of α.

• sets : Set (Set α)

  The set of sets that belong to the filter.

• univ_sets : Set.univ ∈ self.sets

  The set Set.univ belongs to any filter.

• sets_of_superset : ∀ {x y : Set α}, x ∈ self.sets → x ⊆ y → y ∈ self.sets

  If a set belongs to a filter, then its superset belongs to the filter as well.

• inter_sets : ∀ {x y : Set α}, x ∈ self.sets → y ∈ self.sets → x ∩ y ∈ self.sets

  If two sets belong to a filter, then their intersection belongs to the filter as well.

theorem Filter.univ_sets {α : Type u_1} (self : Filter α) : Set.univ ∈ self.sets

The set Set.univ belongs to any filter.

theorem Filter.sets_of_superset {α : Type u_1} (self : Filter α) {x : Set α} {y : Set α} : x ∈ self.sets → x ⊆ y → y ∈ self.sets

If a set belongs to a filter, then its superset belongs to the filter as well.

theorem Filter.inter_sets {α : Type u_1} (self : Filter α) {x : Set α} {y : Set α} : x ∈ self.sets → y ∈ self.sets → x ∩ y ∈ self.sets

If two sets belong to a filter, then their intersection belongs to the filter as well.

instance instMembershipSetFilter {α : Type u_1} : Membership (Set α) (Filter α)

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

Equations

• instMembershipSetFilter = { mem := fun (U : Set α) (F : Filter α) => U ∈ F.sets }

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

@[simp]

theorem Filter.mem_sets {α : Type u} {f : Filter α} {s : Set α} : s ∈ f.sets ↔ s ∈ f

instance Filter.inhabitedMem {α : Type u} {f : Filter α} : Inhabited { s : Set α // s ∈ f }

Equations

• Filter.inhabitedMem = { default := ⟨Set.univ, ⋯⟩ }

theorem Filter.filter_eq {α : Type u} {f : Filter α} {g : Filter α} : f.sets = g.sets → f = g

theorem Filter.filter_eq_iff {α : Type u} {f : Filter α} {g : Filter α} : f = g ↔ f.sets = g.sets

theorem Filter.ext_iff {α : Type u} {f : Filter α} {g : Filter α} : f = g ↔ ∀ (s : Set α), s ∈ f ↔ s ∈ g

theorem Filter.ext {α : Type u} {f : Filter α} {g : Filter α} : (∀ (s : Set α), s ∈ f ↔ s ∈ g) → f = g

theorem Filter.coext {α : Type u} {f : Filter α} {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).

@[simp]

theorem Filter.univ_mem {α : Type u} {f : Filter α} : Set.univ ∈ f

theorem Filter.mem_of_superset {α : Type u} {f : Filter α} {x : Set α} {y : Set α} (hx : x ∈ f) (hxy : x ⊆ y) : y ∈ f

instance Filter.instTransSetSupersetMem {α : Type u} : Trans (fun (x x_1 : Set α) => x ⊇ x_1) (fun (x : Set α) (x_1 : Filter α) => x ∈ x_1) fun (x : Set α) (x_1 : Filter α) => x ∈ x_1

Equations

• Filter.instTransSetSupersetMem = { trans := ⋯ }

theorem Filter.inter_mem {α : Type u} {f : Filter α} {s : Set α} {t : Set α} (hs : s ∈ f) (ht : t ∈ f) : s ∩ t ∈ f

@[simp]

theorem Filter.inter_mem_iff {α : Type u} {f : Filter α} {s : Set α} {t : Set α} : s ∩ t ∈ f ↔ s ∈ f ∧ t ∈ f

theorem Filter.diff_mem {α : Type u} {f : Filter α} {s : Set α} {t : Set α} (hs : s ∈ f) (ht : tᶜ ∈ f) : s \ t ∈ f

theorem Filter.univ_mem' {α : Type u} {f : Filter α} {s : Set α} (h : ∀ (a : α), a ∈ s) : s ∈ f

theorem Filter.mp_mem {α : Type u} {f : Filter α} {s : Set α} {t : Set α} (hs : s ∈ f) (h : {x : α | x ∈ s → x ∈ t} ∈ f) : t ∈ f

theorem Filter.congr_sets {α : Type u} {f : Filter α} {s : Set α} {t : Set α} (h : {x : α | x ∈ s ↔ x ∈ t} ∈ f) : s ∈ f ↔ t ∈ f

def Filter.copy {α : Type u} (f : Filter α) (S : Set (Set α)) (hmem : ∀ (s : Set α), s ∈ S ↔ s ∈ f) : Filter α

Override sets field of a filter to provide better definitional equality.

Equations

• f.copy S hmem = { sets := S, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

theorem Filter.copy_eq {α : Type u} {f : Filter α} {S : Set (Set α)} (hmem : ∀ (s : Set α), s ∈ S ↔ s ∈ f) : f.copy S hmem = f

@[simp]

theorem Filter.mem_copy {α : Type u} {f : Filter α} {s : Set α} {S : Set (Set α)} {hmem : ∀ (s : Set α), s ∈ S ↔ s ∈ f} : s ∈ f.copy S hmem ↔ s ∈ S

@[simp]

theorem Filter.biInter_mem {α : Type u} {f : Filter α} {β : Type v} {s : β → Set α} {is : Set β} (hf : is.Finite) : ⋂ i ∈ is, s i ∈ f ↔ ∀ i ∈ is, s i ∈ f

@[simp]

theorem Filter.biInter_finset_mem {α : Type u} {f : Filter α} {β : Type v} {s : β → Set α} (is : Finset β) : ⋂ i ∈ is, s i ∈ f ↔ ∀ i ∈ is, s i ∈ f

theorem Finset.iInter_mem_sets {α : Type u} {f : Filter α} {β : Type v} {s : β → Set α} (is : Finset β) : ⋂ i ∈ is, s i ∈ f ↔ ∀ i ∈ is, s i ∈ f

Alias of Filter.biInter_finset_mem.

@[simp]

theorem Filter.sInter_mem {α : Type u} {f : Filter α} {s : Set (Set α)} (hfin : s.Finite) : ⋂₀ s ∈ f ↔ ∀ U ∈ s, U ∈ f

@[simp]

theorem Filter.iInter_mem {α : Type u} {f : Filter α} {β : Sort v} {s : β → Set α} [Finite β] : ⋂ (i : β), s i ∈ f ↔ ∀ (i : β), s i ∈ f

theorem Filter.exists_mem_subset_iff {α : Type u} {f : Filter α} {s : Set α} : (∃ t ∈ f, t ⊆ s) ↔ s ∈ f

theorem Filter.monotone_mem {α : Type u} {f : Filter α} : Monotone fun (s : Set α) => s ∈ f

theorem Filter.exists_mem_and_iff {α : Type u} {f : Filter α} {P : Set α → Prop} {Q : Set α → Prop} (hP : Antitone P) (hQ : Antitone Q) : ((∃ u ∈ f, P u) ∧ ∃ u ∈ f, Q u) ↔ ∃ u ∈ f, P u ∧ Q u

theorem Filter.forall_in_swap {α : Type u} {f : Filter α} {β : Type u_1} {p : Set α → β → Prop} : (∀ a ∈ f, ∀ (b : β), p a b) ↔ ∀ (b : β), ∀ a ∈ f, p a b

def Mathlib.Tactic.filterUpwards : Lean.ParserDescr

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.

Equations

• One or more equations did not get rendered due to their size.

def Filter.principal {α : Type u} (s : 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 := ⋯ }

def Filter.term𝓟 : Lean.ParserDescr

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

Equations

• Filter.term𝓟 = Lean.ParserDescr.node `Filter.term𝓟 1024 (Lean.ParserDescr.symbol "𝓟")

@[simp]

theorem Filter.mem_principal {α : Type u} {s : Set α} {t : Set α} : s ∈ Filter.principal t ↔ t ⊆ s

theorem Filter.mem_principal_self {α : Type u} (s : Set α) : s ∈ Filter.principal s

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

• f.join = { sets := {s : Set α | {t : Filter α | s ∈ t} ∈ f}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

@[simp]

theorem Filter.mem_join {α : Type u} {s : Set α} {f : Filter (Filter α)} : s ∈ f.join ↔ {t : Filter α | s ∈ t} ∈ f

instance Filter.instPartialOrder {α : Type u} : PartialOrder (Filter α)

Equations

• Filter.instPartialOrder = PartialOrder.mk ⋯

theorem Filter.le_def {α : Type u} {f : Filter α} {g : Filter α} : f ≤ g ↔ ∀ x ∈ g, x ∈ f

theorem Filter.not_le {α : Type u} {f : Filter α} {g : Filter α} : ¬f ≤ g ↔ ∃ s ∈ g, s ∉ f

inductive Filter.GenerateSets {α : Type u} (g : Set (Set α)) : Set α → Prop

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

• basic: ∀ {α : Type u} {g : Set (Set α)} {s : Set α}, s ∈ g → Filter.GenerateSets g s
• univ: ∀ {α : Type u} {g : Set (Set α)}, Filter.GenerateSets g Set.univ
• superset: ∀ {α : Type u} {g : Set (Set α)} {s t : Set α}, Filter.GenerateSets g s → s ⊆ t → Filter.GenerateSets g t
• inter: ∀ {α : Type u} {g : Set (Set α)} {s t : Set α}, Filter.GenerateSets g s → Filter.GenerateSets g t → Filter.GenerateSets g (s ∩ t)

def Filter.generate {α : Type u} (g : Set (Set α)) : Filter α

generate g is the largest filter containing the sets g.

Equations

• Filter.generate g = { sets := {s : Set α | Filter.GenerateSets g s}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

theorem Filter.mem_generate_of_mem {α : Type u} {s : Set (Set α)} {U : Set α} (h : U ∈ s) : U ∈ Filter.generate s

theorem Filter.le_generate_iff {α : Type u} {s : Set (Set α)} {f : Filter α} : f ≤ Filter.generate s ↔ s ⊆ f.sets

theorem Filter.mem_generate_iff {α : Type u} {s : Set (Set α)} {U : Set α} : U ∈ Filter.generate s ↔ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U

@[simp]

theorem Filter.generate_singleton {α : Type u} (s : Set α) : Filter.generate {s} = Filter.principal s

def Filter.mkOfClosure {α : Type u} (s : Set (Set α)) (hs : (Filter.generate s).sets = s) : Filter α

mkOfClosure 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.mkOfClosure s hs = { sets := s, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

theorem Filter.mkOfClosure_sets {α : Type u} {s : Set (Set α)} {hs : (Filter.generate s).sets = s} : Filter.mkOfClosure s hs = Filter.generate s

def Filter.giGenerate (α : Type u_2) : GaloisInsertion Filter.generate Filter.sets

Galois insertion from sets of sets into filters.

Equations

• Filter.giGenerate α = { choice := fun (s : Set (Set α)) (hs : (Filter.generate s).sets ≤ s) => Filter.mkOfClosure s ⋯, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }

instance Filter.instInf {α : Type u} : Inf (Filter α)

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

Equations

• Filter.instInf = { inf := fun (f g : Filter α) => { sets := {s : Set α | ∃ a ∈ f, ∃ b ∈ g, s = a ∩ b}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } }

theorem Filter.mem_inf_iff {α : Type u} {f : Filter α} {g : Filter α} {s : Set α} : s ∈ f ⊓ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, s = t₁ ∩ t₂

theorem Filter.mem_inf_of_left {α : Type u} {f : Filter α} {g : Filter α} {s : Set α} (h : s ∈ f) : s ∈ f ⊓ g

theorem Filter.mem_inf_of_right {α : Type u} {f : Filter α} {g : Filter α} {s : Set α} (h : s ∈ g) : s ∈ f ⊓ g

theorem Filter.inter_mem_inf {α : Type u} {f : Filter α} {g : Filter α} {s : Set α} {t : Set α} (hs : s ∈ f) (ht : t ∈ g) : s ∩ t ∈ f ⊓ g

theorem Filter.mem_inf_of_inter {α : Type u} {f : Filter α} {g : Filter α} {s : Set α} {t : Set α} {u : Set α} (hs : s ∈ f) (ht : t ∈ g) (h : s ∩ t ⊆ u) : u ∈ f ⊓ g

theorem Filter.mem_inf_iff_superset {α : Type u} {f : Filter α} {g : Filter α} {s : Set α} : s ∈ f ⊓ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ∩ t₂ ⊆ s

instance Filter.instTop {α : Type u} : Top (Filter α)

Equations

• Filter.instTop = { top := { sets := {s : Set α | ∀ (x : α), x ∈ s}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } }

theorem Filter.mem_top_iff_forall {α : Type u} {s : Set α} : s ∈ ⊤ ↔ ∀ (x : α), x ∈ s

@[simp]

theorem Filter.mem_top {α : Type u} {s : Set α} : s ∈ ⊤ ↔ s = Set.univ

instance Filter.instCompleteLatticeFilter {α : Type u} : CompleteLattice (Filter α)

Equations

• Filter.instCompleteLatticeFilter = let __src := OrderDual.instCompleteLattice; CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance Filter.instInhabited {α : Type u} : Inhabited (Filter α)

Equations

• Filter.instInhabited = { default := ⊥ }

class Filter.NeBot {α : Type u} (f : Filter α) : Prop

A filter is NeBot 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 CompleteLattice structure on Filter _, so we use a typeclass argument in lemmas instead.

• ne' : f ≠ ⊥

  The filter is nontrivial: f ≠ ⊥ or equivalently, ∅ ∉ f.

theorem Filter.NeBot.ne' {α : Type u} {f : Filter α} [self : f.NeBot] : f ≠ ⊥

The filter is nontrivial: f ≠ ⊥ or equivalently, ∅ ∉ f.

theorem Filter.neBot_iff {α : Type u} {f : Filter α} : f.NeBot ↔ f ≠ ⊥

theorem Filter.NeBot.ne {α : Type u} {f : Filter α} (hf : f.NeBot) : f ≠ ⊥

@[simp]

theorem Filter.not_neBot {α : Type u} {f : Filter α} : ¬f.NeBot ↔ f = ⊥

theorem Filter.NeBot.mono {α : Type u} {f : Filter α} {g : Filter α} (hf : f.NeBot) (hg : f ≤ g) : g.NeBot

theorem Filter.neBot_of_le {α : Type u} {f : Filter α} {g : Filter α} [hf : f.NeBot] (hg : f ≤ g) : g.NeBot

@[simp]

theorem Filter.sup_neBot {α : Type u} {f : Filter α} {g : Filter α} : (f ⊔ g).NeBot ↔ f.NeBot ∨ g.NeBot

theorem Filter.not_disjoint_self_iff {α : Type u} {f : Filter α} : ¬Disjoint f f ↔ f.NeBot

theorem Filter.bot_sets_eq {α : Type u} : ⊥.sets = Set.univ

theorem Filter.eq_or_neBot {α : Type u} (f : Filter α) : f = ⊥ ∨ f.NeBot

Either f = ⊥ or Filter.NeBot f. This is a version of eq_or_ne that uses Filter.NeBot as the second alternative, to be used as an instance.

theorem Filter.sup_sets_eq {α : Type u} {f : Filter α} {g : Filter α} : (f ⊔ g).sets = f.sets ∩ g.sets

theorem Filter.sSup_sets_eq {α : Type u} {s : Set (Filter α)} : (sSup s).sets = ⋂ f ∈ s, f.sets

theorem Filter.iSup_sets_eq {α : Type u} {ι : Sort x} {f : ι → Filter α} : (iSup f).sets = ⋂ (i : ι), (f i).sets

theorem Filter.generate_empty {α : Type u} : Filter.generate ∅ = ⊤

theorem Filter.generate_univ {α : Type u} : Filter.generate Set.univ = ⊥

theorem Filter.generate_union {α : Type u} {s : Set (Set α)} {t : Set (Set α)} : Filter.generate (s ∪ t) = Filter.generate s ⊓ Filter.generate t

theorem Filter.generate_iUnion {α : Type u} {ι : Sort x} {s : ι → Set (Set α)} : Filter.generate (⋃ (i : ι), s i) = ⨅ (i : ι), Filter.generate (s i)

@[simp]

theorem Filter.mem_bot {α : Type u} {s : Set α} : s ∈ ⊥

@[simp]

theorem Filter.mem_sup {α : Type u} {f : Filter α} {g : Filter α} {s : Set α} : s ∈ f ⊔ g ↔ s ∈ f ∧ s ∈ g

theorem Filter.union_mem_sup {α : Type u} {f : Filter α} {g : Filter α} {s : Set α} {t : Set α} (hs : s ∈ f) (ht : t ∈ g) : s ∪ t ∈ f ⊔ g

@[simp]

theorem Filter.mem_sSup {α : Type u} {x : Set α} {s : Set (Filter α)} : x ∈ sSup s ↔ ∀ f ∈ s, x ∈ f

@[simp]

theorem Filter.mem_iSup {α : Type u} {ι : Sort x} {x : Set α} {f : ι → Filter α} : x ∈ iSup f ↔ ∀ (i : ι), x ∈ f i

@[simp]

theorem Filter.iSup_neBot {α : Type u} {ι : Sort x} {f : ι → Filter α} : (⨆ (i : ι), f i).NeBot ↔ ∃ (i : ι), (f i).NeBot

theorem Filter.iInf_eq_generate {α : Type u} {ι : Sort x} (s : ι → Filter α) : iInf s = Filter.generate (⋃ (i : ι), (s i).sets)

theorem Filter.mem_iInf_of_mem {α : Type u} {ι : Sort x} {f : ι → Filter α} (i : ι) {s : Set α} (hs : s ∈ f i) : s ∈ ⨅ (i : ι), f i

theorem Filter.mem_iInf_of_iInter {α : Type u} {ι : Type u_2} {s : ι → Filter α} {U : Set α} {I : Set ι} (I_fin : I.Finite) {V : ↑I → Set α} (hV : ∀ (i : ↑I), V i ∈ s ↑i) (hU : ⋂ (i : ↑I), V i ⊆ U) : U ∈ ⨅ (i : ι), s i

theorem Filter.mem_iInf {α : Type u} {ι : Type u_2} {s : ι → Filter α} {U : Set α} : U ∈ ⨅ (i : ι), s i ↔ ∃ (I : Set ι), I.Finite ∧ ∃ (V : ↑I → Set α), (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ (i : ↑I), V i

theorem Filter.mem_iInf' {α : Type u} {ι : Type u_2} {s : ι → Filter α} {U : Set α} : U ∈ ⨅ (i : ι), s i ↔ ∃ (I : Set ι), I.Finite ∧ ∃ (V : ι → Set α), (∀ (i : ι), V i ∈ s i) ∧ (∀ i ∉ I, V i = Set.univ) ∧ U = ⋂ i ∈ I, V i ∧ U = ⋂ (i : ι), V i

theorem Filter.exists_iInter_of_mem_iInf {ι : Type u_2} {α : Type u_3} {f : ι → Filter α} {s : Set α} (hs : s ∈ ⨅ (i : ι), f i) : ∃ (t : ι → Set α), (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ (i : ι), t i

theorem Filter.mem_iInf_of_finite {ι : Type u_2} [Finite ι] {α : Type u_3} {f : ι → Filter α} (s : Set α) : s ∈ ⨅ (i : ι), f i ↔ ∃ (t : ι → Set α), (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ (i : ι), t i

@[simp]

theorem Filter.le_principal_iff {α : Type u} {s : Set α} {f : Filter α} : f ≤ Filter.principal s ↔ s ∈ f

theorem Filter.Iic_principal {α : Type u} (s : Set α) : Set.Iic (Filter.principal s) = {l : Filter α | s ∈ l}

theorem Filter.principal_mono {α : Type u} {s : Set α} {t : Set α} : Filter.principal s ≤ Filter.principal t ↔ s ⊆ t

theorem GCongr.filter_principal_mono {α : Type u} {s : Set α} {t : Set α} : s ⊆ t → Filter.principal s ≤ Filter.principal t

Alias of the reverse direction of Filter.principal_mono.

theorem Filter.monotone_principal {α : Type u} : Monotone Filter.principal

@[simp]

theorem Filter.principal_eq_iff_eq {α : Type u} {s : Set α} {t : Set α} : Filter.principal s = Filter.principal t ↔ s = t

@[simp]

theorem Filter.join_principal_eq_sSup {α : Type u} {s : Set (Filter α)} : (Filter.principal s).join = sSup s

@[simp]

theorem Filter.principal_univ {α : Type u} : Filter.principal Set.univ = ⊤

@[simp]

theorem Filter.principal_empty {α : Type u} : Filter.principal ∅ = ⊥

theorem Filter.generate_eq_biInf {α : Type u} (S : Set (Set α)) : Filter.generate S = ⨅ s ∈ S, Filter.principal s

Lattice equations

theorem Filter.empty_mem_iff_bot {α : Type u} {f : Filter α} : ∅ ∈ f ↔ f = ⊥

theorem Filter.nonempty_of_mem {α : Type u} {f : Filter α} [hf : f.NeBot] {s : Set α} (hs : s ∈ f) : s.Nonempty

theorem Filter.NeBot.nonempty_of_mem {α : Type u} {f : Filter α} (hf : f.NeBot) {s : Set α} (hs : s ∈ f) : s.Nonempty

@[simp]

theorem Filter.empty_not_mem {α : Type u} (f : Filter α) [f.NeBot] : ∅ ∉ f

theorem Filter.nonempty_of_neBot {α : Type u} (f : Filter α) [f.NeBot] : Nonempty α

theorem Filter.compl_not_mem {α : Type u} {f : Filter α} {s : Set α} [f.NeBot] (h : s ∈ f) : sᶜ ∉ f

theorem Filter.filter_eq_bot_of_isEmpty {α : Type u} [IsEmpty α] (f : Filter α) : f = ⊥

theorem Filter.disjoint_iff {α : Type u} {f : Filter α} {g : Filter α} : Disjoint f g ↔ ∃ s ∈ f, ∃ t ∈ g, Disjoint s t

theorem Filter.disjoint_of_disjoint_of_mem {α : Type u} {f : Filter α} {g : Filter α} {s : Set α} {t : Set α} (h : Disjoint s t) (hs : s ∈ f) (ht : t ∈ g) : Disjoint f g

theorem Filter.NeBot.not_disjoint {α : Type u} {f : Filter α} {s : Set α} {t : Set α} (hf : f.NeBot) (hs : s ∈ f) (ht : t ∈ f) : ¬Disjoint s t

theorem Filter.inf_eq_bot_iff {α : Type u} {f : Filter α} {g : Filter α} : f ⊓ g = ⊥ ↔ ∃ U ∈ f, ∃ V ∈ g, U ∩ V = ∅

theorem Pairwise.exists_mem_filter_of_disjoint {α : Type u} {ι : Type u_2} [Finite ι] {l : ι → Filter α} (hd : Pairwise (Disjoint on l)) : ∃ (s : ι → Set α), (∀ (i : ι), s i ∈ l i) ∧ Pairwise (Disjoint on s)

theorem Set.PairwiseDisjoint.exists_mem_filter {α : Type u} {ι : Type u_2} {l : ι → Filter α} {t : Set ι} (hd : t.PairwiseDisjoint l) (ht : t.Finite) : ∃ (s : ι → Set α), (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s

instance Filter.unique {α : Type u} [IsEmpty α] : Unique (Filter α)

There is exactly one filter on an empty type.

Equations

• Filter.unique = { default := ⊥, uniq := ⋯ }

theorem Filter.NeBot.nonempty {α : Type u} (f : Filter α) [hf : f.NeBot] : Nonempty α

theorem Filter.eq_top_of_neBot {α : Type u} [Subsingleton α] (l : Filter α) [l.NeBot] : l = ⊤

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

theorem Filter.forall_mem_nonempty_iff_neBot {α : Type u} {f : Filter α} : (∀ s ∈ f, s.Nonempty) ↔ f.NeBot

instance Filter.instNontrivialFilter {α : Type u} [Nonempty α] : Nontrivial (Filter α)

Equations

• ⋯ = ⋯

theorem Filter.nontrivial_iff_nonempty {α : Type u} : Nontrivial (Filter α) ↔ Nonempty α

theorem Filter.eq_sInf_of_mem_iff_exists_mem {α : Type u} {S : Set (Filter α)} {l : Filter α} (h : ∀ {s : Set α}, s ∈ l ↔ ∃ f ∈ S, s ∈ f) : l = sInf S

theorem Filter.eq_iInf_of_mem_iff_exists_mem {α : Type u} {ι : Sort x} {f : ι → Filter α} {l : Filter α} (h : ∀ {s : Set α}, s ∈ l ↔ ∃ (i : ι), s ∈ f i) : l = iInf f

theorem Filter.eq_biInf_of_mem_iff_exists_mem {α : Type u} {ι : Sort x} {f : ι → Filter α} {p : ι → Prop} {l : Filter α} (h : ∀ {s : Set α}, s ∈ l ↔ ∃ (i : ι), p i ∧ s ∈ f i) : l = ⨅ (i : ι), ⨅ (_ : p i), f i

theorem Filter.iInf_sets_eq {α : Type u} {ι : Sort x} {f : ι → Filter α} (h : Directed (fun (x x_1 : Filter α) => x ≥ x_1) f) [ne : Nonempty ι] : (iInf f).sets = ⋃ (i : ι), (f i).sets

theorem Filter.mem_iInf_of_directed {α : Type u} {ι : Sort x} {f : ι → Filter α} (h : Directed (fun (x x_1 : Filter α) => x ≥ x_1) f) [Nonempty ι] (s : Set α) : s ∈ iInf f ↔ ∃ (i : ι), s ∈ f i

theorem Filter.mem_biInf_of_directed {α : Type u} {β : Type v} {f : β → Filter α} {s : Set β} (h : DirectedOn (f ⁻¹'o fun (x x_1 : Filter α) => x ≥ x_1) s) (ne : s.Nonempty) {t : Set α} : t ∈ ⨅ i ∈ s, f i ↔ ∃ i ∈ s, t ∈ f i

theorem Filter.biInf_sets_eq {α : Type u} {β : Type v} {f : β → Filter α} {s : Set β} (h : DirectedOn (f ⁻¹'o fun (x x_1 : Filter α) => x ≥ x_1) s) (ne : s.Nonempty) : (⨅ i ∈ s, f i).sets = ⋃ i ∈ s, (f i).sets

theorem Filter.iInf_sets_eq_finite {α : Type u} {ι : Type u_2} (f : ι → Filter α) : (⨅ (i : ι), f i).sets = ⋃ (t : Finset ι), (⨅ i ∈ t, f i).sets

theorem Filter.iInf_sets_eq_finite' {α : Type u} {ι : Sort x} (f : ι → Filter α) : (⨅ (i : ι), f i).sets = ⋃ (t : Finset (PLift ι)), (⨅ i ∈ t, f i.down).sets

theorem Filter.mem_iInf_finite {α : Type u} {ι : Type u_2} {f : ι → Filter α} (s : Set α) : s ∈ iInf f ↔ ∃ (t : Finset ι), s ∈ ⨅ i ∈ t, f i

theorem Filter.mem_iInf_finite' {α : Type u} {ι : Sort x} {f : ι → Filter α} (s : Set α) : s ∈ iInf f ↔ ∃ (t : Finset (PLift ι)), s ∈ ⨅ i ∈ t, f i.down

@[simp]

theorem Filter.sup_join {α : Type u} {f₁ : Filter (Filter α)} {f₂ : Filter (Filter α)} : f₁.join ⊔ f₂.join = (f₁ ⊔ f₂).join

@[simp]

theorem Filter.iSup_join {α : Type u} {ι : Sort w} {f : ι → Filter (Filter α)} : ⨆ (x : ι), (f x).join = (⨆ (x : ι), f x).join

instance Filter.instDistribLattice {α : Type u} : DistribLattice (Filter α)

Equations

• Filter.instDistribLattice = let __src := Filter.instCompleteLatticeFilter; DistribLattice.mk ⋯

instance Filter.instCoframe {α : Type u} : Order.Coframe (Filter α)

Equations

• Filter.instCoframe = let __src := Filter.instCompleteLatticeFilter; Order.Coframe.mk ⋯

theorem Filter.mem_iInf_finset {α : Type u} {β : Type v} {s : Finset α} {f : α → Filter β} {t : Set β} : t ∈ ⨅ a ∈ s, f a ↔ ∃ (p : α → Set β), (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ a ∈ s, p a

theorem Filter.iInf_neBot_of_directed' {α : Type u} {ι : Sort x} {f : ι → Filter α} [Nonempty ι] (hd : Directed (fun (x x_1 : Filter α) => x ≥ x_1) f) : (∀ (i : ι), (f i).NeBot) → (iInf f).NeBot

If f : ι → Filter α is directed, ι is not empty, and ∀ i, f i ≠ ⊥, then iInf f ≠ ⊥. See also iInf_neBot_of_directed for a version assuming Nonempty α instead of Nonempty ι.

theorem Filter.iInf_neBot_of_directed {α : Type u} {ι : Sort x} {f : ι → Filter α} [hn : Nonempty α] (hd : Directed (fun (x x_1 : Filter α) => x ≥ x_1) f) (hb : ∀ (i : ι), (f i).NeBot) : (iInf f).NeBot

If f : ι → Filter α is directed, α is not empty, and ∀ i, f i ≠ ⊥, then iInf f ≠ ⊥. See also iInf_neBot_of_directed' for a version assuming Nonempty ι instead of Nonempty α.

theorem Filter.sInf_neBot_of_directed' {α : Type u} {s : Set (Filter α)} (hne : s.Nonempty) (hd : DirectedOn (fun (x x_1 : Filter α) => x ≥ x_1) s) (hbot : ⊥ ∉ s) : (sInf s).NeBot

theorem Filter.sInf_neBot_of_directed {α : Type u} [Nonempty α] {s : Set (Filter α)} (hd : DirectedOn (fun (x x_1 : Filter α) => x ≥ x_1) s) (hbot : ⊥ ∉ s) : (sInf s).NeBot

theorem Filter.iInf_neBot_iff_of_directed' {α : Type u} {ι : Sort x} {f : ι → Filter α} [Nonempty ι] (hd : Directed (fun (x x_1 : Filter α) => x ≥ x_1) f) : (iInf f).NeBot ↔ ∀ (i : ι), (f i).NeBot

theorem Filter.iInf_neBot_iff_of_directed {α : Type u} {ι : Sort x} {f : ι → Filter α} [Nonempty α] (hd : Directed (fun (x x_1 : Filter α) => x ≥ x_1) f) : (iInf f).NeBot ↔ ∀ (i : ι), (f i).NeBot

theorem Filter.iInf_sets_induct {α : Type u} {ι : Sort x} {f : ι → Filter α} {s : Set α} (hs : s ∈ iInf 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

@[simp]

theorem Filter.inf_principal {α : Type u} {s : Set α} {t : Set α} : Filter.principal s ⊓ Filter.principal t = Filter.principal (s ∩ t)

@[simp]

theorem Filter.sup_principal {α : Type u} {s : Set α} {t : Set α} : Filter.principal s ⊔ Filter.principal t = Filter.principal (s ∪ t)

@[simp]

theorem Filter.iSup_principal {α : Type u} {ι : Sort w} {s : ι → Set α} : ⨆ (x : ι), Filter.principal (s x) = Filter.principal (⋃ (i : ι), s i)

@[simp]

theorem Filter.principal_eq_bot_iff {α : Type u} {s : Set α} : Filter.principal s = ⊥ ↔ s = ∅

@[simp]

theorem Filter.principal_neBot_iff {α : Type u} {s : Set α} : (Filter.principal s).NeBot ↔ s.Nonempty

theorem Set.Nonempty.principal_neBot {α : Type u} {s : Set α} : s.Nonempty → (Filter.principal s).NeBot

Alias of the reverse direction of Filter.principal_neBot_iff.

theorem Filter.isCompl_principal {α : Type u} (s : Set α) : IsCompl (Filter.principal s) (Filter.principal sᶜ)

theorem Filter.mem_inf_principal' {α : Type u} {f : Filter α} {s : Set α} {t : Set α} : s ∈ f ⊓ Filter.principal t ↔ tᶜ ∪ s ∈ f

theorem Filter.mem_inf_principal {α : Type u} {f : Filter α} {s : Set α} {t : Set α} : s ∈ f ⊓ Filter.principal t ↔ {x : α | x ∈ t → x ∈ s} ∈ f

theorem Filter.iSup_inf_principal {α : Type u} {ι : Sort x} (f : ι → Filter α) (s : Set α) : ⨆ (i : ι), f i ⊓ Filter.principal s = (⨆ (i : ι), f i) ⊓ Filter.principal s

theorem Filter.inf_principal_eq_bot {α : Type u} {f : Filter α} {s : Set α} : f ⊓ Filter.principal s = ⊥ ↔ sᶜ ∈ f

theorem Filter.mem_of_eq_bot {α : Type u} {f : Filter α} {s : Set α} (h : f ⊓ Filter.principal sᶜ = ⊥) : s ∈ f

theorem Filter.diff_mem_inf_principal_compl {α : Type u} {f : Filter α} {s : Set α} (hs : s ∈ f) (t : Set α) : s \ t ∈ f ⊓ Filter.principal tᶜ

theorem Filter.principal_le_iff {α : Type u} {s : Set α} {f : Filter α} : Filter.principal s ≤ f ↔ ∀ V ∈ f, s ⊆ V

@[simp]

theorem Filter.iInf_principal_finset {α : Type u} {ι : Type w} (s : Finset ι) (f : ι → Set α) : ⨅ i ∈ s, Filter.principal (f i) = Filter.principal (⋂ i ∈ s, f i)

theorem Filter.iInf_principal {α : Type u} {ι : Sort w} [Finite ι] (f : ι → Set α) : ⨅ (i : ι), Filter.principal (f i) = Filter.principal (⋂ (i : ι), f i)

@[simp]

theorem Filter.iInf_principal' {α : Type u} {ι : Type w} [Finite ι] (f : ι → Set α) : ⨅ (i : ι), Filter.principal (f i) = Filter.principal (⋂ (i : ι), f i)

A special case of iInf_principal that is safe to mark simp.

theorem Filter.iInf_principal_finite {α : Type u} {ι : Type w} {s : Set ι} (hs : s.Finite) (f : ι → Set α) : ⨅ i ∈ s, Filter.principal (f i) = Filter.principal (⋂ i ∈ s, f i)

theorem Filter.join_mono {α : Type u} {f₁ : Filter (Filter α)} {f₂ : Filter (Filter α)} (h : f₁ ≤ f₂) : f₁.join ≤ f₂.join

Eventually

def Filter.Eventually {α : Type u} (p : α → Prop) (f : Filter α) : Prop

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

Equations

• Filter.Eventually p f = ({x : α | p x} ∈ f)

def Filter.«term∀ᶠ_In_,_».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def Filter.«term∀ᶠ_In_,_» : Lean.ParserDescr

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

Equations

• One or more equations did not get rendered due to their size.

theorem Filter.eventually_iff {α : Type u} {f : Filter α} {P : α → Prop} : (∀ᶠ (x : α) in f, P x) ↔ {x : α | P x} ∈ f

@[simp]

theorem Filter.eventually_mem_set {α : Type u} {s : Set α} {l : Filter α} : (∀ᶠ (x : α) in l, x ∈ s) ↔ s ∈ l

theorem Filter.ext' {α : Type u} {f₁ : Filter α} {f₂ : Filter α} (h : ∀ (p : α → Prop), (∀ᶠ (x : α) in f₁, p x) ↔ ∀ᶠ (x : α) in f₂, p x) : f₁ = f₂

theorem Filter.Eventually.filter_mono {α : Type u} {f₁ : Filter α} {f₂ : Filter α} (h : f₁ ≤ f₂) {p : α → Prop} (hp : ∀ᶠ (x : α) in f₂, p x) : ∀ᶠ (x : α) in f₁, p x

theorem Filter.eventually_of_mem {α : Type u} {f : Filter α} {P : α → Prop} {U : Set α} (hU : U ∈ f) (h : ∀ x ∈ U, P x) : ∀ᶠ (x : α) in f, P x

theorem Filter.Eventually.and {α : Type u} {p : α → Prop} {q : α → Prop} {f : Filter α} : Filter.Eventually p f → Filter.Eventually q f → ∀ᶠ (x : α) in f, p x ∧ q x

@[simp]

theorem Filter.eventually_true {α : Type u} (f : Filter α) : ∀ᶠ (x : α) in f, True

theorem Filter.eventually_of_forall {α : Type u} {p : α → Prop} {f : Filter α} (hp : ∀ (x : α), p x) : ∀ᶠ (x : α) in f, p x

@[simp]

theorem Filter.eventually_false_iff_eq_bot {α : Type u} {f : Filter α} : (∀ᶠ (x : α) in f, False) ↔ f = ⊥

@[simp]

theorem Filter.eventually_const {α : Type u} {f : Filter α} [t : f.NeBot] {p : Prop} : (∀ᶠ (x : α) in f, p) ↔ p

theorem Filter.eventually_iff_exists_mem {α : Type u} {p : α → Prop} {f : Filter α} : (∀ᶠ (x : α) in f, p x) ↔ ∃ v ∈ f, ∀ y ∈ v, p y

theorem Filter.Eventually.exists_mem {α : Type u} {p : α → Prop} {f : Filter α} (hp : ∀ᶠ (x : α) in f, p x) : ∃ v ∈ f, ∀ y ∈ v, p y

theorem Filter.Eventually.mp {α : Type u} {p : α → Prop} {q : α → Prop} {f : Filter α} (hp : ∀ᶠ (x : α) in f, p x) (hq : ∀ᶠ (x : α) in f, p x → q x) : ∀ᶠ (x : α) in f, q x

theorem Filter.Eventually.mono {α : Type u} {p : α → Prop} {q : α → Prop} {f : Filter α} (hp : ∀ᶠ (x : α) in f, p x) (hq : ∀ (x : α), p x → q x) : ∀ᶠ (x : α) in f, q x

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

@[simp]

theorem Filter.eventually_and {α : Type u} {p : α → Prop} {q : α → Prop} {f : Filter α} : (∀ᶠ (x : α) in f, p x ∧ q x) ↔ (∀ᶠ (x : α) in f, p x) ∧ ∀ᶠ (x : α) in f, q x

theorem Filter.Eventually.congr {α : Type u} {f : Filter α} {p : α → Prop} {q : α → Prop} (h' : ∀ᶠ (x : α) in f, p x) (h : ∀ᶠ (x : α) in f, p x ↔ q x) : ∀ᶠ (x : α) in f, q x

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

@[simp]

theorem Filter.eventually_all {α : Type u} {ι : Sort u_2} [Finite ι] {l : Filter α} {p : ι → α → Prop} : (∀ᶠ (x : α) in l, ∀ (i : ι), p i x) ↔ ∀ (i : ι), ∀ᶠ (x : α) in l, p i x

@[simp]

theorem Filter.eventually_all_finite {α : Type u} {ι : Type u_2} {I : Set ι} (hI : I.Finite) {l : Filter α} {p : ι → α → Prop} : (∀ᶠ (x : α) in l, ∀ i ∈ I, p i x) ↔ ∀ i ∈ I, ∀ᶠ (x : α) in l, p i x

theorem Set.Finite.eventually_all {α : Type u} {ι : Type u_2} {I : Set ι} (hI : I.Finite) {l : Filter α} {p : ι → α → Prop} : (∀ᶠ (x : α) in l, ∀ i ∈ I, p i x) ↔ ∀ i ∈ I, ∀ᶠ (x : α) in l, p i x

Alias of Filter.eventually_all_finite.

@[simp]

theorem Filter.eventually_all_finset {α : Type u} {ι : Type u_2} (I : Finset ι) {l : Filter α} {p : ι → α → Prop} : (∀ᶠ (x : α) in l, ∀ i ∈ I, p i x) ↔ ∀ i ∈ I, ∀ᶠ (x : α) in l, p i x

theorem Finset.eventually_all {α : Type u} {ι : Type u_2} (I : Finset ι) {l : Filter α} {p : ι → α → Prop} : (∀ᶠ (x : α) in l, ∀ i ∈ I, p i x) ↔ ∀ i ∈ I, ∀ᶠ (x : α) in l, p i x

Alias of Filter.eventually_all_finset.

@[simp]

theorem Filter.eventually_or_distrib_left {α : Type u} {f : Filter α} {p : Prop} {q : α → Prop} : (∀ᶠ (x : α) in f, p ∨ q x) ↔ p ∨ ∀ᶠ (x : α) in f, q x

@[simp]

theorem Filter.eventually_or_distrib_right {α : Type u} {f : Filter α} {p : α → Prop} {q : Prop} : (∀ᶠ (x : α) in f, p x ∨ q) ↔ (∀ᶠ (x : α) in f, p x) ∨ q

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

@[simp]

theorem Filter.eventually_bot {α : Type u} {p : α → Prop} : ∀ᶠ (x : α) in ⊥, p x

@[simp]

theorem Filter.eventually_top {α : Type u} {p : α → Prop} : (∀ᶠ (x : α) in ⊤, p x) ↔ ∀ (x : α), p x

@[simp]

theorem Filter.eventually_sup {α : Type u} {p : α → Prop} {f : Filter α} {g : Filter α} : (∀ᶠ (x : α) in f ⊔ g, p x) ↔ (∀ᶠ (x : α) in f, p x) ∧ ∀ᶠ (x : α) in g, p x

@[simp]

theorem Filter.eventually_sSup {α : Type u} {p : α → Prop} {fs : Set (Filter α)} : (∀ᶠ (x : α) in sSup fs, p x) ↔ ∀ f ∈ fs, ∀ᶠ (x : α) in f, p x

@[simp]

theorem Filter.eventually_iSup {α : Type u} {ι : Sort x} {p : α → Prop} {fs : ι → Filter α} : (∀ᶠ (x : α) in ⨆ (b : ι), fs b, p x) ↔ ∀ (b : ι), ∀ᶠ (x : α) in fs b, p x

@[simp]

theorem Filter.eventually_principal {α : Type u} {a : Set α} {p : α → Prop} : (∀ᶠ (x : α) in Filter.principal a, p x) ↔ ∀ x ∈ a, p x

theorem Filter.Eventually.forall_mem {α : Type u_2} {f : Filter α} {s : Set α} {P : α → Prop} (hP : ∀ᶠ (x : α) in f, P x) (hf : Filter.principal s ≤ f) (x : α) : x ∈ s → P x

theorem Filter.eventually_inf {α : Type u} {f : Filter α} {g : Filter α} {p : α → Prop} : (∀ᶠ (x : α) in f ⊓ g, p x) ↔ ∃ s ∈ f, ∃ t ∈ g, ∀ x ∈ s ∩ t, p x

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

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 atTop, p x means that there exist arbitrarily large x for which p holds true.

Equations

• Filter.Frequently p f = ¬∀ᶠ (x : α) in f, ¬p x

def Filter.«term∃ᶠ_In_,_» : Lean.ParserDescr

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

Equations

• One or more equations did not get rendered due to their size.

def Filter.«term∃ᶠ_In_,_».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

theorem Filter.Eventually.frequently {α : Type u} {f : Filter α} [f.NeBot] {p : α → Prop} (h : ∀ᶠ (x : α) in f, p x) : ∃ᶠ (x : α) in f, p x

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

theorem Filter.Frequently.mp {α : Type u} {p : α → Prop} {q : α → Prop} {f : Filter α} (h : ∃ᶠ (x : α) in f, p x) (hpq : ∀ᶠ (x : α) in f, p x → q x) : ∃ᶠ (x : α) in f, q x

theorem Filter.Frequently.filter_mono {α : Type u} {p : α → Prop} {f : Filter α} {g : Filter α} (h : ∃ᶠ (x : α) in f, p x) (hle : f ≤ g) : ∃ᶠ (x : α) in g, p x

theorem Filter.Frequently.mono {α : Type u} {p : α → Prop} {q : α → Prop} {f : Filter α} (h : ∃ᶠ (x : α) in f, p x) (hpq : ∀ (x : α), p x → q x) : ∃ᶠ (x : α) in f, q x

theorem Filter.Frequently.and_eventually {α : Type u} {p : α → Prop} {q : α → Prop} {f : Filter α} (hp : ∃ᶠ (x : α) in f, p x) (hq : ∀ᶠ (x : α) in f, q x) : ∃ᶠ (x : α) in f, p x ∧ q x

theorem Filter.Eventually.and_frequently {α : Type u} {p : α → Prop} {q : α → Prop} {f : Filter α} (hp : ∀ᶠ (x : α) in f, p x) (hq : ∃ᶠ (x : α) in f, q x) : ∃ᶠ (x : α) in f, p x ∧ q x

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

theorem Filter.Eventually.exists {α : Type u} {p : α → Prop} {f : Filter α} [f.NeBot] (hp : ∀ᶠ (x : α) in f, p x) : ∃ (x : α), p x

theorem Filter.frequently_iff_neBot {α : Type u} {l : Filter α} {p : α → Prop} : (∃ᶠ (x : α) in l, p x) ↔ (l ⊓ Filter.principal {x : α | p x}).NeBot

theorem Filter.frequently_mem_iff_neBot {α : Type u} {l : Filter α} {s : Set α} : (∃ᶠ (x : α) in l, x ∈ s) ↔ (l ⊓ Filter.principal s).NeBot

theorem Filter.frequently_iff_forall_eventually_exists_and {α : Type u} {p : α → Prop} {f : Filter α} : (∃ᶠ (x : α) in f, p x) ↔ ∀ {q : α → Prop}, (∀ᶠ (x : α) in f, q x) → ∃ (x : α), p x ∧ q x

theorem Filter.frequently_iff {α : Type u} {f : Filter α} {P : α → Prop} : (∃ᶠ (x : α) in f, P x) ↔ ∀ {U : Set α}, U ∈ f → ∃ x ∈ U, P x

@[simp]

theorem Filter.not_eventually {α : Type u} {p : α → Prop} {f : Filter α} : (¬∀ᶠ (x : α) in f, p x) ↔ ∃ᶠ (x : α) in f, ¬p x

@[simp]

theorem Filter.not_frequently {α : Type u} {p : α → Prop} {f : Filter α} : (¬∃ᶠ (x : α) in f, p x) ↔ ∀ᶠ (x : α) in f, ¬p x

@[simp]

theorem Filter.frequently_true_iff_neBot {α : Type u} (f : Filter α) : (∃ᶠ (x : α) in f, True) ↔ f.NeBot

@[simp]

theorem Filter.frequently_false {α : Type u} (f : Filter α) : ¬∃ᶠ (x : α) in f, False

@[simp]

theorem Filter.frequently_const {α : Type u} {f : Filter α} [f.NeBot] {p : Prop} : (∃ᶠ (x : α) in f, p) ↔ p

@[simp]

theorem Filter.frequently_or_distrib {α : Type u} {f : Filter α} {p : α → Prop} {q : α → Prop} : (∃ᶠ (x : α) in f, p x ∨ q x) ↔ (∃ᶠ (x : α) in f, p x) ∨ ∃ᶠ (x : α) in f, q x

theorem Filter.frequently_or_distrib_left {α : Type u} {f : Filter α} [f.NeBot] {p : Prop} {q : α → Prop} : (∃ᶠ (x : α) in f, p ∨ q x) ↔ p ∨ ∃ᶠ (x : α) in f, q x

theorem Filter.frequently_or_distrib_right {α : Type u} {f : Filter α} [f.NeBot] {p : α → Prop} {q : Prop} : (∃ᶠ (x : α) in f, p x ∨ q) ↔ (∃ᶠ (x : α) in f, p x) ∨ q

theorem Filter.frequently_imp_distrib {α : Type u} {f : Filter α} {p : α → Prop} {q : α → Prop} : (∃ᶠ (x : α) in f, p x → q x) ↔ (∀ᶠ (x : α) in f, p x) → ∃ᶠ (x : α) in f, q x

theorem Filter.frequently_imp_distrib_left {α : Type u} {f : Filter α} [f.NeBot] {p : Prop} {q : α → Prop} : (∃ᶠ (x : α) in f, p → q x) ↔ p → ∃ᶠ (x : α) in f, q x

theorem Filter.frequently_imp_distrib_right {α : Type u} {f : Filter α} [f.NeBot] {p : α → Prop} {q : Prop} : (∃ᶠ (x : α) in f, p x → q) ↔ (∀ᶠ (x : α) in f, p x) → q

theorem Filter.eventually_imp_distrib_right {α : Type u} {f : Filter α} {p : α → Prop} {q : Prop} : (∀ᶠ (x : α) in f, p x → q) ↔ (∃ᶠ (x : α) in f, p x) → q

@[simp]

theorem Filter.frequently_and_distrib_left {α : Type u} {f : Filter α} {p : Prop} {q : α → Prop} : (∃ᶠ (x : α) in f, p ∧ q x) ↔ p ∧ ∃ᶠ (x : α) in f, q x

@[simp]

theorem Filter.frequently_and_distrib_right {α : Type u} {f : Filter α} {p : α → Prop} {q : Prop} : (∃ᶠ (x : α) in f, p x ∧ q) ↔ (∃ᶠ (x : α) in f, p x) ∧ q

@[simp]

theorem Filter.frequently_bot {α : Type u} {p : α → Prop} : ¬∃ᶠ (x : α) in ⊥, p x

@[simp]

theorem Filter.frequently_top {α : Type u} {p : α → Prop} : (∃ᶠ (x : α) in ⊤, p x) ↔ ∃ (x : α), p x

@[simp]

theorem Filter.frequently_principal {α : Type u} {a : Set α} {p : α → Prop} : (∃ᶠ (x : α) in Filter.principal a, p x) ↔ ∃ x ∈ a, p x

theorem Filter.frequently_inf_principal {α : Type u} {f : Filter α} {s : Set α} {p : α → Prop} : (∃ᶠ (x : α) in f ⊓ Filter.principal s, p x) ↔ ∃ᶠ (x : α) in f, x ∈ s ∧ p x

theorem Filter.Frequently.inf_principal {α : Type u} {f : Filter α} {s : Set α} {p : α → Prop} : (∃ᶠ (x : α) in f, x ∈ s ∧ p x) → ∃ᶠ (x : α) in f ⊓ Filter.principal s, p x

Alias of the reverse direction of Filter.frequently_inf_principal.

theorem Filter.Frequently.of_inf_principal {α : Type u} {f : Filter α} {s : Set α} {p : α → Prop} : (∃ᶠ (x : α) in f ⊓ Filter.principal s, p x) → ∃ᶠ (x : α) in f, x ∈ s ∧ p x

Alias of the forward direction of Filter.frequently_inf_principal.

theorem Filter.frequently_sup {α : Type u} {p : α → Prop} {f : Filter α} {g : Filter α} : (∃ᶠ (x : α) in f ⊔ g, p x) ↔ (∃ᶠ (x : α) in f, p x) ∨ ∃ᶠ (x : α) in g, p x

@[simp]

theorem Filter.frequently_sSup {α : Type u} {p : α → Prop} {fs : Set (Filter α)} : (∃ᶠ (x : α) in sSup fs, p x) ↔ ∃ f ∈ fs, ∃ᶠ (x : α) in f, p x

@[simp]

theorem Filter.frequently_iSup {α : Type u} {β : Type v} {p : α → Prop} {fs : β → Filter α} : (∃ᶠ (x : α) in ⨆ (b : β), fs b, p x) ↔ ∃ (b : β), ∃ᶠ (x : α) in fs b, p x

theorem Filter.Eventually.choice {α : Type u} {β : Type v} {r : α → β → Prop} {l : Filter α} [l.NeBot] (h : ∀ᶠ (x : α) in l, ∃ (y : β), r x y) : ∃ (f : α → β), ∀ᶠ (x : α) in l, r x (f x)

Relation “eventually equal”

def Filter.EventuallyEq {α : Type u} {β : Type v} (l : Filter α) (f : α → β) (g : α → β) : Prop

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

Equations

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

def Filter.«term_=ᶠ[_]_» : Lean.TrailingParserDescr

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

• One or more equations did not get rendered due to their size.

theorem Filter.EventuallyEq.eventually {α : Type u} {β : Type v} {l : Filter α} {f : α → β} {g : α → β} (h : f =ᶠ[l] g) : ∀ᶠ (x : α) in l, f x = g x

theorem Filter.EventuallyEq.rw {α : Type u} {β : Type v} {l : Filter α} {f : α → β} {g : α → β} (h : f =ᶠ[l] g) (p : α → β → Prop) (hf : ∀ᶠ (x : α) in l, p x (f x)) : ∀ᶠ (x : α) in l, p x (g x)

theorem Filter.eventuallyEq_set {α : Type u} {s : Set α} {t : Set α} {l : Filter α} : s =ᶠ[l] t ↔ ∀ᶠ (x : α) in l, x ∈ s ↔ x ∈ t

theorem Filter.Eventually.set_eq {α : Type u} {s : Set α} {t : Set α} {l : Filter α} : (∀ᶠ (x : α) in l, x ∈ s ↔ x ∈ t) → s =ᶠ[l] t

Alias of the reverse direction of Filter.eventuallyEq_set.

theorem Filter.EventuallyEq.mem_iff {α : Type u} {s : Set α} {t : Set α} {l : Filter α} : s =ᶠ[l] t → ∀ᶠ (x : α) in l, x ∈ s ↔ x ∈ t

Alias of the forward direction of Filter.eventuallyEq_set.

@[simp]

theorem Filter.eventuallyEq_univ {α : Type u} {s : Set α} {l : Filter α} : s =ᶠ[l] Set.univ ↔ s ∈ l

theorem Filter.EventuallyEq.exists_mem {α : Type u} {β : Type v} {l : Filter α} {f : α → β} {g : α → β} (h : f =ᶠ[l] g) : ∃ s ∈ l, Set.EqOn f g s

theorem Filter.eventuallyEq_of_mem {α : Type u} {β : Type v} {l : Filter α} {f : α → β} {g : α → β} {s : Set α} (hs : s ∈ l) (h : Set.EqOn f g s) : f =ᶠ[l] g

theorem Filter.eventuallyEq_iff_exists_mem {α : Type u} {β : Type v} {l : Filter α} {f : α → β} {g : α → β} : f =ᶠ[l] g ↔ ∃ s ∈ l, Set.EqOn f g s

theorem Filter.EventuallyEq.filter_mono {α : Type u} {β : Type v} {l : Filter α} {l' : Filter α} {f : α → β} {g : α → β} (h₁ : f =ᶠ[l] g) (h₂ : l' ≤ l) : f =ᶠ[l'] g

@[simp]

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

theorem Filter.EventuallyEq.rfl {α : Type u} {β : Type v} {l : Filter α} {f : α → β} : f =ᶠ[l] f

theorem Filter.EventuallyEq.symm {α : Type u} {β : Type v} {f : α → β} {g : α → β} {l : Filter α} (H : f =ᶠ[l] g) : g =ᶠ[l] f

theorem Filter.EventuallyEq.trans {α : Type u} {β : Type v} {l : Filter α} {f : α → β} {g : α → β} {h : α → β} (H₁ : f =ᶠ[l] g) (H₂ : g =ᶠ[l] h) : f =ᶠ[l] h

instance Filter.instTransForallEventuallyEq {α : Type u} {β : Type v} {l : Filter α} : Trans (fun (x x_1 : α → β) => x =ᶠ[l] x_1) (fun (x x_1 : α → β) => x =ᶠ[l] x_1) fun (x x_1 : α → β) => x =ᶠ[l] x_1

Equations

• Filter.instTransForallEventuallyEq = { trans := ⋯ }

theorem Filter.EventuallyEq.prod_mk {α : Type u} {β : Type v} {γ : Type w} {l : Filter α} {f : α → β} {f' : α → β} (hf : f =ᶠ[l] f') {g : α → γ} {g' : α → γ} (hg : g =ᶠ[l] g') : (fun (x : α) => (f x, g x)) =ᶠ[l] fun (x : α) => (f' x, g' x)

theorem Filter.EventuallyEq.fun_comp {α : Type u} {β : Type v} {γ : Type w} {f : α → β} {g : α → β} {l : Filter α} (H : f =ᶠ[l] g) (h : β → γ) : h ∘ f =ᶠ[l] h ∘ g

theorem Filter.EventuallyEq.comp₂ {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_2} {f : α → β} {f' : α → β} {g : α → γ} {g' : α → γ} {l : Filter α} (Hf : f =ᶠ[l] f') (h : β → γ → δ) (Hg : g =ᶠ[l] g') : (fun (x : α) => h (f x) (g x)) =ᶠ[l] fun (x : α) => h (f' x) (g' x)

theorem Filter.EventuallyEq.add {α : Type u} {β : Type v} [Add β] {f : α → β} {f' : α → β} {g : α → β} {g' : α → β} {l : Filter α} (h : f =ᶠ[l] g) (h' : f' =ᶠ[l] g') : (fun (x : α) => f x + f' x) =ᶠ[l] fun (x : α) => g x + g' x

theorem Filter.EventuallyEq.mul {α : Type u} {β : Type v} [Mul β] {f : α → β} {f' : α → β} {g : α → β} {g' : α → β} {l : Filter α} (h : f =ᶠ[l] g) (h' : f' =ᶠ[l] g') : (fun (x : α) => f x * f' x) =ᶠ[l] fun (x : α) => g x * g' x

theorem Filter.EventuallyEq.const_smul {α : Type u} {β : Type v} {γ : Type u_2} [SMul γ β] {f : α → β} {g : α → β} {l : Filter α} (h : f =ᶠ[l] g) (c : γ) : (fun (x : α) => c • f x) =ᶠ[l] fun (x : α) => c • g x

theorem Filter.EventuallyEq.pow_const {α : Type u} {β : Type v} {γ : Type u_2} [Pow β γ] {f : α → β} {g : α → β} {l : Filter α} (h : f =ᶠ[l] g) (c : γ) : (fun (x : α) => f x ^ c) =ᶠ[l] fun (x : α) => g x ^ c

theorem Filter.EventuallyEq.neg {α : Type u} {β : Type v} [Neg β] {f : α → β} {g : α → β} {l : Filter α} (h : f =ᶠ[l] g) : (fun (x : α) => -f x) =ᶠ[l] fun (x : α) => -g x

theorem Filter.EventuallyEq.inv {α : Type u} {β : Type v} [Inv β] {f : α → β} {g : α → β} {l : Filter α} (h : f =ᶠ[l] g) : (fun (x : α) => (f x)⁻¹) =ᶠ[l] fun (x : α) => (g x)⁻¹

theorem Filter.EventuallyEq.sub {α : Type u} {β : Type v} [Sub β] {f : α → β} {f' : α → β} {g : α → β} {g' : α → β} {l : Filter α} (h : f =ᶠ[l] g) (h' : f' =ᶠ[l] g') : (fun (x : α) => f x - f' x) =ᶠ[l] fun (x : α) => g x - g' x

theorem Filter.EventuallyEq.div {α : Type u} {β : Type v} [Div β] {f : α → β} {f' : α → β} {g : α → β} {g' : α → β} {l : Filter α} (h : f =ᶠ[l] g) (h' : f' =ᶠ[l] g') : (fun (x : α) => f x / f' x) =ᶠ[l] fun (x : α) => g x / g' x

theorem Filter.EventuallyEq.const_vadd {α : Type u} {β : Type v} {γ : Type u_2} [VAdd γ β] {f : α → β} {g : α → β} {l : Filter α} (h : f =ᶠ[l] g) (c : γ) : (fun (x : α) => c +ᵥ f x) =ᶠ[l] fun (x : α) => c +ᵥ g x

theorem Filter.EventuallyEq.vadd {α : Type u} {β : Type v} {𝕜 : Type u_2} [VAdd 𝕜 β] {l : Filter α} {f : α → 𝕜} {f' : α → 𝕜} {g : α → β} {g' : α → β} (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') : (fun (x : α) => f x +ᵥ g x) =ᶠ[l] fun (x : α) => f' x +ᵥ g' x

theorem Filter.EventuallyEq.smul {α : Type u} {β : Type v} {𝕜 : Type u_2} [SMul 𝕜 β] {l : Filter α} {f : α → 𝕜} {f' : α → 𝕜} {g : α → β} {g' : α → β} (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') : (fun (x : α) => f x • g x) =ᶠ[l] fun (x : α) => f' x • g' x

theorem Filter.EventuallyEq.sup {α : Type u} {β : Type v} [Sup β] {l : Filter α} {f : α → β} {f' : α → β} {g : α → β} {g' : α → β} (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') : (fun (x : α) => f x ⊔ g x) =ᶠ[l] fun (x : α) => f' x ⊔ g' x

theorem Filter.EventuallyEq.inf {α : Type u} {β : Type v} [Inf β] {l : Filter α} {f : α → β} {f' : α → β} {g : α → β} {g' : α → β} (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') : (fun (x : α) => f x ⊓ g x) =ᶠ[l] fun (x : α) => f' x ⊓ g' x

theorem Filter.EventuallyEq.preimage {α : Type u} {β : Type v} {l : Filter α} {f : α → β} {g : α → β} (h : f =ᶠ[l] g) (s : Set β) : f ⁻¹' s =ᶠ[l] g ⁻¹' s

theorem Filter.EventuallyEq.inter {α : Type u} {s : Set α} {t : Set α} {s' : Set α} {t' : Set α} {l : Filter α} (h : s =ᶠ[l] t) (h' : s' =ᶠ[l] t') : s ∩ s' =ᶠ[l] t ∩ t'

theorem Filter.EventuallyEq.union {α : Type u} {s : Set α} {t : Set α} {s' : Set α} {t' : Set α} {l : Filter α} (h : s =ᶠ[l] t) (h' : s' =ᶠ[l] t') : s ∪ s' =ᶠ[l] t ∪ t'

theorem Filter.EventuallyEq.compl {α : Type u} {s : Set α} {t : Set α} {l : Filter α} (h : s =ᶠ[l] t) : sᶜ =ᶠ[l] tᶜ

theorem Filter.EventuallyEq.diff {α : Type u} {s : Set α} {t : Set α} {s' : Set α} {t' : Set α} {l : Filter α} (h : s =ᶠ[l] t) (h' : s' =ᶠ[l] t') : s \ s' =ᶠ[l] t \ t'

theorem Filter.eventuallyEq_empty {α : Type u} {s : Set α} {l : Filter α} : s =ᶠ[l] ∅ ↔ ∀ᶠ (x : α) in l, x ∉ s

theorem Filter.inter_eventuallyEq_left {α : Type u} {s : Set α} {t : Set α} {l : Filter α} : s ∩ t =ᶠ[l] s ↔ ∀ᶠ (x : α) in l, x ∈ s → x ∈ t

theorem Filter.inter_eventuallyEq_right {α : Type u} {s : Set α} {t : Set α} {l : Filter α} : s ∩ t =ᶠ[l] t ↔ ∀ᶠ (x : α) in l, x ∈ t → x ∈ s

@[simp]

theorem Filter.eventuallyEq_principal {α : Type u} {β : Type v} {s : Set α} {f : α → β} {g : α → β} : f =ᶠ[Filter.principal s] g ↔ Set.EqOn f g s

theorem Filter.eventuallyEq_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

theorem Filter.EventuallyEq.sub_eq {α : Type u} {β : Type v} [AddGroup β] {f : α → β} {g : α → β} {l : Filter α} (h : f =ᶠ[l] g) : f - g =ᶠ[l] 0

theorem Filter.eventuallyEq_iff_sub {α : Type u} {β : Type v} [AddGroup β] {f : α → β} {g : α → β} {l : Filter α} : f =ᶠ[l] g ↔ f - g =ᶠ[l] 0

def Filter.EventuallyLE {α : Type u} {β : Type v} [LE β] (l : Filter α) (f : α → β) (g : α → β) : 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

def Filter.«term_≤ᶠ[_]_» : Lean.TrailingParserDescr

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

Equations

• One or more equations did not get rendered due to their size.

theorem Filter.EventuallyLE.congr {α : Type u} {β : Type v} [LE β] {l : Filter α} {f : α → β} {f' : α → β} {g : α → β} {g' : α → β} (H : f ≤ᶠ[l] g) (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') : f' ≤ᶠ[l] g'

theorem Filter.eventuallyLE_congr {α : Type u} {β : Type v} [LE β] {l : Filter α} {f : α → β} {f' : α → β} {g : α → β} {g' : α → β} (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') : f ≤ᶠ[l] g ↔ f' ≤ᶠ[l] g'

theorem Filter.EventuallyEq.le {α : Type u} {β : Type v} [Preorder β] {l : Filter α} {f : α → β} {g : α → β} (h : f =ᶠ[l] g) : f ≤ᶠ[l] g

theorem Filter.EventuallyLE.refl {α : Type u} {β : Type v} [Preorder β] (l : Filter α) (f : α → β) : f ≤ᶠ[l] f

theorem Filter.EventuallyLE.rfl {α : Type u} {β : Type v} [Preorder β] {l : Filter α} {f : α → β} : f ≤ᶠ[l] f

theorem Filter.EventuallyLE.trans {α : Type u} {β : Type v} [Preorder β] {l : Filter α} {f : α → β} {g : α → β} {h : α → β} (H₁ : f ≤ᶠ[l] g) (H₂ : g ≤ᶠ[l] h) : f ≤ᶠ[l] h

instance Filter.instTransForallEventuallyLE {α : Type u} {β : Type v} [Preorder β] {l : Filter α} : Trans (fun (x x_1 : α → β) => x ≤ᶠ[l] x_1) (fun (x x_1 : α → β) => x ≤ᶠ[l] x_1) fun (x x_1 : α → β) => x ≤ᶠ[l] x_1

Equations

• Filter.instTransForallEventuallyLE = { trans := ⋯ }

theorem Filter.EventuallyEq.trans_le {α : Type u} {β : Type v} [Preorder β] {l : Filter α} {f : α → β} {g : α → β} {h : α → β} (H₁ : f =ᶠ[l] g) (H₂ : g ≤ᶠ[l] h) : f ≤ᶠ[l] h

instance Filter.instTransForallEventuallyEqEventuallyLE {α : Type u} {β : Type v} [Preorder β] {l : Filter α} : Trans (fun (x x_1 : α → β) => x =ᶠ[l] x_1) (fun (x x_1 : α → β) => x ≤ᶠ[l] x_1) fun (x x_1 : α → β) => x ≤ᶠ[l] x_1

Equations

• Filter.instTransForallEventuallyEqEventuallyLE = { trans := ⋯ }

theorem Filter.EventuallyLE.trans_eq {α : Type u} {β : Type v} [Preorder β] {l : Filter α} {f : α → β} {g : α → β} {h : α → β} (H₁ : f ≤ᶠ[l] g) (H₂ : g =ᶠ[l] h) : f ≤ᶠ[l] h

instance Filter.instTransForallEventuallyLEEventuallyEq {α : Type u} {β : Type v} [Preorder β] {l : Filter α} : Trans (fun (x x_1 : α → β) => x ≤ᶠ[l] x_1) (fun (x x_1 : α → β) => x =ᶠ[l] x_1) fun (x x_1 : α → β) => x ≤ᶠ[l] x_1

Equations

• Filter.instTransForallEventuallyLEEventuallyEq = { trans := ⋯ }

theorem Filter.EventuallyLE.antisymm {α : Type u} {β : Type v} [PartialOrder β] {l : Filter α} {f : α → β} {g : α → β} (h₁ : f ≤ᶠ[l] g) (h₂ : g ≤ᶠ[l] f) : f =ᶠ[l] g

theorem Filter.eventuallyLE_antisymm_iff {α : Type u} {β : Type v} [PartialOrder β] {l : Filter α} {f : α → β} {g : α → β} : f =ᶠ[l] g ↔ f ≤ᶠ[l] g ∧ g ≤ᶠ[l] f

theorem Filter.EventuallyLE.le_iff_eq {α : Type u} {β : Type v} [PartialOrder β] {l : Filter α} {f : α → β} {g : α → β} (h : f ≤ᶠ[l] g) : g ≤ᶠ[l] f ↔ g =ᶠ[l] f

theorem Filter.Eventually.ne_of_lt {α : Type u} {β : Type v} [Preorder β] {l : Filter α} {f : α → β} {g : α → β} (h : ∀ᶠ (x : α) in l, f x < g x) : ∀ᶠ (x : α) in l, f x ≠ g x

theorem Filter.Eventually.ne_top_of_lt {α : Type u} {β : Type v} [PartialOrder β] [OrderTop β] {l : Filter α} {f : α → β} {g : α → β} (h : ∀ᶠ (x : α) in l, f x < g x) : ∀ᶠ (x : α) in l, f x ≠ ⊤

theorem Filter.Eventually.lt_top_of_ne {α : Type u} {β : Type v} [PartialOrder β] [OrderTop β] {l : Filter α} {f : α → β} (h : ∀ᶠ (x : α) in l, f x ≠ ⊤) : ∀ᶠ (x : α) in l, f x < ⊤

theorem Filter.Eventually.lt_top_iff_ne_top {α : Type u} {β : Type v} [PartialOrder β] [OrderTop β] {l : Filter α} {f : α → β} : (∀ᶠ (x : α) in l, f x < ⊤) ↔ ∀ᶠ (x : α) in l, f x ≠ ⊤

theorem Filter.EventuallyLE.inter {α : Type u} {s : Set α} {t : Set α} {s' : Set α} {t' : Set α} {l : Filter α} (h : s ≤ᶠ[l] t) (h' : s' ≤ᶠ[l] t') : s ∩ s' ≤ᶠ[l] t ∩ t'

theorem Filter.EventuallyLE.union {α : Type u} {s : Set α} {t : Set α} {s' : Set α} {t' : Set α} {l : Filter α} (h : s ≤ᶠ[l] t) (h' : s' ≤ᶠ[l] t') : s ∪ s' ≤ᶠ[l] t ∪ t'

theorem Filter.EventuallyLE.iUnion {α : Type u} {ι : Sort x} {l : Filter α} [Finite ι] {s : ι → Set α} {t : ι → Set α} (h : ∀ (i : ι), s i ≤ᶠ[l] t i) : ⋃ (i : ι), s i ≤ᶠ[l] ⋃ (i : ι), t i

theorem Filter.EventuallyEq.iUnion {α : Type u} {ι : Sort x} {l : Filter α} [Finite ι] {s : ι → Set α} {t : ι → Set α} (h : ∀ (i : ι), s i =ᶠ[l] t i) : ⋃ (i : ι), s i =ᶠ[l] ⋃ (i : ι), t i

theorem Filter.EventuallyLE.iInter {α : Type u} {ι : Sort x} {l : Filter α} [Finite ι] {s : ι → Set α} {t : ι → Set α} (h : ∀ (i : ι), s i ≤ᶠ[l] t i) : ⋂ (i : ι), s i ≤ᶠ[l] ⋂ (i : ι), t i

theorem Filter.EventuallyEq.iInter {α : Type u} {ι : Sort x} {l : Filter α} [Finite ι] {s : ι → Set α} {t : ι → Set α} (h : ∀ (i : ι), s i =ᶠ[l] t i) : ⋂ (i : ι), s i =ᶠ[l] ⋂ (i : ι), t i

theorem Set.Finite.eventuallyLE_iUnion {α : Type u} {l : Filter α} {ι : Type u_2} {s : Set ι} (hs : s.Finite) {f : ι → Set α} {g : ι → Set α} (hle : ∀ i ∈ s, f i ≤ᶠ[l] g i) : ⋃ i ∈ s, f i ≤ᶠ[l] ⋃ i ∈ s, g i

theorem Filter.EventuallyLE.biUnion {α : Type u} {l : Filter α} {ι : Type u_2} {s : Set ι} (hs : s.Finite) {f : ι → Set α} {g : ι → Set α} (hle : ∀ i ∈ s, f i ≤ᶠ[l] g i) : ⋃ i ∈ s, f i ≤ᶠ[l] ⋃ i ∈ s, g i

Alias of Set.Finite.eventuallyLE_iUnion.

theorem Set.Finite.eventuallyEq_iUnion {α : Type u} {l : Filter α} {ι : Type u_2} {s : Set ι} (hs : s.Finite) {f : ι → Set α} {g : ι → Set α} (heq : ∀ i ∈ s, f i =ᶠ[l] g i) : ⋃ i ∈ s, f i =ᶠ[l] ⋃ i ∈ s, g i

theorem Filter.EventuallyEq.biUnion {α : Type u} {l : Filter α} {ι : Type u_2} {s : Set ι} (hs : s.Finite) {f : ι → Set α} {g : ι → Set α} (heq : ∀ i ∈ s, f i =ᶠ[l] g i) : ⋃ i ∈ s, f i =ᶠ[l] ⋃ i ∈ s, g i

Alias of Set.Finite.eventuallyEq_iUnion.

theorem Set.Finite.eventuallyLE_iInter {α : Type u} {l : Filter α} {ι : Type u_2} {s : Set ι} (hs : s.Finite) {f : ι → Set α} {g : ι → Set α} (hle : ∀ i ∈ s, f i ≤ᶠ[l] g i) : ⋂ i ∈ s, f i ≤ᶠ[l] ⋂ i ∈ s, g i

theorem Filter.EventuallyLE.biInter {α : Type u} {l : Filter α} {ι : Type u_2} {s : Set ι} (hs : s.Finite) {f : ι → Set α} {g : ι → Set α} (hle : ∀ i ∈ s, f i ≤ᶠ[l] g i) : ⋂ i ∈ s, f i ≤ᶠ[l] ⋂ i ∈ s, g i

Alias of Set.Finite.eventuallyLE_iInter.

theorem Set.Finite.eventuallyEq_iInter {α : Type u} {l : Filter α} {ι : Type u_2} {s : Set ι} (hs : s.Finite) {f : ι → Set α} {g : ι → Set α} (heq : ∀ i ∈ s, f i =ᶠ[l] g i) : ⋂ i ∈ s, f i =ᶠ[l] ⋂ i ∈ s, g i

theorem Filter.EventuallyEq.biInter {α : Type u} {l : Filter α} {ι : Type u_2} {s : Set ι} (hs : s.Finite) {f : ι → Set α} {g : ι → Set α} (heq : ∀ i ∈ s, f i =ᶠ[l] g i) : ⋂ i ∈ s, f i =ᶠ[l] ⋂ i ∈ s, g i

Alias of Set.Finite.eventuallyEq_iInter.

theorem Finset.eventuallyLE_iUnion {α : Type u} {l : Filter α} {ι : Type u_2} (s : Finset ι) {f : ι → Set α} {g : ι → Set α} (hle : ∀ i ∈ s, f i ≤ᶠ[l] g i) : ⋃ i ∈ s, f i ≤ᶠ[l] ⋃ i ∈ s, g i

theorem Finset.eventuallyEq_iUnion {α : Type u} {l : Filter α} {ι : Type u_2} (s : Finset ι) {f : ι → Set α} {g : ι → Set α} (heq : ∀ i ∈ s, f i =ᶠ[l] g i) : ⋃ i ∈ s, f i =ᶠ[l] ⋃ i ∈ s, g i

theorem Finset.eventuallyLE_iInter {α : Type u} {l : Filter α} {ι : Type u_2} (s : Finset ι) {f : ι → Set α} {g : ι → Set α} (hle : ∀ i ∈ s, f i ≤ᶠ[l] g i) : ⋂ i ∈ s, f i ≤ᶠ[l] ⋂ i ∈ s, g i

theorem Finset.eventuallyEq_iInter {α : Type u} {l : Filter α} {ι : Type u_2} (s : Finset ι) {f : ι → Set α} {g : ι → Set α} (heq : ∀ i ∈ s, f i =ᶠ[l] g i) : ⋂ i ∈ s, f i =ᶠ[l] ⋂ i ∈ s, g i

theorem Filter.EventuallyLE.compl {α : Type u} {s : Set α} {t : Set α} {l : Filter α} (h : s ≤ᶠ[l] t) : tᶜ ≤ᶠ[l] sᶜ

theorem Filter.EventuallyLE.diff {α : Type u} {s : Set α} {t : Set α} {s' : Set α} {t' : Set α} {l : Filter α} (h : s ≤ᶠ[l] t) (h' : t' ≤ᶠ[l] s') : s \ s' ≤ᶠ[l] t \ t'

theorem Filter.set_eventuallyLE_iff_mem_inf_principal {α : Type u} {s : Set α} {t : Set α} {l : Filter α} : s ≤ᶠ[l] t ↔ t ∈ l ⊓ Filter.principal s

theorem Filter.set_eventuallyLE_iff_inf_principal_le {α : Type u} {s : Set α} {t : Set α} {l : Filter α} : s ≤ᶠ[l] t ↔ l ⊓ Filter.principal s ≤ l ⊓ Filter.principal t

theorem Filter.set_eventuallyEq_iff_inf_principal {α : Type u} {s : Set α} {t : Set α} {l : Filter α} : s =ᶠ[l] t ↔ l ⊓ Filter.principal s = l ⊓ Filter.principal t

theorem Filter.EventuallyLE.sup {α : Type u} {β : Type v} [SemilatticeSup β] {l : Filter α} {f₁ : α → β} {f₂ : α → β} {g₁ : α → β} {g₂ : α → β} (hf : f₁ ≤ᶠ[l] f₂) (hg : g₁ ≤ᶠ[l] g₂) : f₁ ⊔ g₁ ≤ᶠ[l] f₂ ⊔ g₂

theorem Filter.EventuallyLE.sup_le {α : Type u} {β : Type v} [SemilatticeSup β] {l : Filter α} {f : α → β} {g : α → β} {h : α → β} (hf : f ≤ᶠ[l] h) (hg : g ≤ᶠ[l] h) : f ⊔ g ≤ᶠ[l] h

theorem Filter.EventuallyLE.le_sup_of_le_left {α : Type u} {β : Type v} [SemilatticeSup β] {l : Filter α} {f : α → β} {g : α → β} {h : α → β} (hf : h ≤ᶠ[l] f) : h ≤ᶠ[l] f ⊔ g

theorem Filter.EventuallyLE.le_sup_of_le_right {α : Type u} {β : Type v} [SemilatticeSup β] {l : Filter α} {f : α → β} {g : α → β} {h : α → β} (hg : h ≤ᶠ[l] g) : h ≤ᶠ[l] f ⊔ g

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

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

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

@[simp]

theorem Filter.map_principal {α : Type u} {β : Type v} {s : Set α} {f : α → β} : Filter.map f (Filter.principal s) = Filter.principal (f '' s)

@[simp]

theorem Filter.eventually_map {α : Type u} {β : Type v} {f : Filter α} {m : α → β} {P : β → Prop} : (∀ᶠ (b : β) in Filter.map m f, P b) ↔ ∀ᶠ (a : α) in f, P (m a)

@[simp]

theorem Filter.frequently_map {α : Type u} {β : Type v} {f : Filter α} {m : α → β} {P : β → Prop} : (∃ᶠ (b : β) in Filter.map m f, P b) ↔ ∃ᶠ (a : α) in f, P (m a)

@[simp]

theorem Filter.mem_map {α : Type u} {β : Type v} {f : Filter α} {m : α → β} {t : Set β} : t ∈ Filter.map m f ↔ m ⁻¹' t ∈ f

theorem Filter.mem_map' {α : Type u} {β : Type v} {f : Filter α} {m : α → β} {t : Set β} : t ∈ Filter.map m f ↔ {x : α | m x ∈ t} ∈ f

theorem Filter.image_mem_map {α : Type u} {β : Type v} {f : Filter α} {m : α → β} {s : Set α} (hs : s ∈ f) : m '' s ∈ Filter.map m f

@[simp]

theorem Filter.image_mem_map_iff {α : Type u} {β : Type v} {f : Filter α} {m : α → β} {s : Set α} (hf : Function.Injective m) : m '' s ∈ Filter.map m f ↔ s ∈ f

theorem Filter.range_mem_map {α : Type u} {β : Type v} {f : Filter α} {m : α → β} : Set.range m ∈ Filter.map m f

theorem Filter.mem_map_iff_exists_image {α : Type u} {β : Type v} {f : Filter α} {m : α → β} {t : Set β} : t ∈ Filter.map m f ↔ ∃ s ∈ f, m '' s ⊆ t

@[simp]

theorem Filter.map_id {α : Type u} {f : Filter α} : Filter.map id f = f

@[simp]

theorem Filter.map_id' {α : Type u} {f : Filter α} : Filter.map (fun (x : α) => x) f = f

@[simp]

theorem Filter.map_compose {α : Type u} {β : Type v} {γ : Type w} {m : α → β} {m' : β → γ} : Filter.map m' ∘ Filter.map m = Filter.map (m' ∘ m)

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

theorem Filter.map_congr {α : Type u} {β : Type v} {m₁ : α → β} {m₂ : α → β} {f : Filter α} (h : m₁ =ᶠ[f] m₂) : Filter.map m₁ f = Filter.map m₂ f

If functions m₁ and m₂ are eventually equal at a filter f, then they map this filter to the same filter.

def Filter.comap {α : Type u} {β : Type v} (m : α → β) (f : Filter β) : 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 kernImage m s = {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

• Filter.comap m f = { sets := {s : Set α | ∃ t ∈ f, m ⁻¹' t ⊆ s}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

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

theorem Filter.mem_comap'' {α : Type u} {β : Type v} {f : α → β} {l : Filter β} {s : Set α} : s ∈ Filter.comap f l ↔ Set.kernImage f s ∈ l

theorem Filter.mem_comap_prod_mk {α : Type u} {β : Type v} {x : α} {s : Set β} {F : Filter (α × β)} : s ∈ Filter.comap (Prod.mk x) F ↔ {p : α × β | p.1 = x → p.2 ∈ s} ∈ F

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

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

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

theorem Filter.mem_comap_iff_compl {α : Type u} {β : Type v} {f : α → β} {l : Filter β} {s : Set α} : s ∈ Filter.comap f l ↔ (f '' sᶜ)ᶜ ∈ l

theorem Filter.compl_mem_comap {α : Type u} {β : Type v} {f : α → β} {l : Filter β} {s : Set α} : sᶜ ∈ Filter.comap f l ↔ (f '' s)ᶜ ∈ l

def Filter.kernMap {α : Type u} {β : Type v} (m : α → β) (f : Filter α) : Filter β

The analog of kernImage for filters. A set s belongs to Filter.kernMap m f if either of the following equivalent conditions hold.

1. There exists a set t ∈ f such that s = kernImage m t. This is used as a definition.
2. There exists a set t such that tᶜ ∈ f and sᶜ = m '' t, see Filter.mem_kernMap_iff_compl and Filter.compl_mem_kernMap.

This definition because it gives a right adjoint to Filter.comap, and because it has a nice interpretation when working with co- filters (Filter.cocompact, Filter.cofinite, ...). For example, kernMap m (cocompact α) is the filter generated by the complements of the sets m '' K where K is a compact subset of α.

Equations

• Filter.kernMap m f = { sets := Set.kernImage m '' f.sets, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

theorem Filter.mem_kernMap {α : Type u} {β : Type v} {m : α → β} {f : Filter α} {s : Set β} : s ∈ Filter.kernMap m f ↔ ∃ t ∈ f, Set.kernImage m t = s

theorem Filter.mem_kernMap_iff_compl {α : Type u} {β : Type v} {m : α → β} {f : Filter α} {s : Set β} : s ∈ Filter.kernMap m f ↔ ∃ (t : Set α), tᶜ ∈ f ∧ m '' t = sᶜ

theorem Filter.compl_mem_kernMap {α : Type u} {β : Type v} {m : α → β} {f : Filter α} {s : Set β} : sᶜ ∈ Filter.kernMap m f ↔ ∃ (t : Set α), tᶜ ∈ f ∧ m '' t = s

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

• f.bind m = (Filter.map m f).join

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

• f.seq g = { sets := {s : Set β | ∃ u ∈ f, ∃ t ∈ g, ∀ m ∈ u, ∀ x ∈ t, m x ∈ s}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

instance Filter.instPure : 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.instPure = { pure := fun {α : Type u_2} (x : α) => { sets := {s : Set α | x ∈ s}, univ_sets := trivial, sets_of_superset := ⋯, inter_sets := ⋯ } }

instance Filter.instBind : Bind Filter

Equations

• Filter.instBind = { bind := @Filter.bind }

instance Filter.instFunctor : Functor Filter

Equations

• Filter.instFunctor = { map := @Filter.map, mapConst := fun {α β : Type u_2} => Filter.map ∘ Function.const β }

instance Filter.instLawfulFunctor : LawfulFunctor Filter

Equations

• Filter.instLawfulFunctor = ⋯

theorem Filter.pure_sets {α : Type u} (a : α) : (pure a).sets = {s : Set α | a ∈ s}

@[simp]

theorem Filter.mem_pure {α : Type u} {a : α} {s : Set α} : s ∈ pure a ↔ a ∈ s

@[simp]

theorem Filter.eventually_pure {α : Type u} {a : α} {p : α → Prop} : (∀ᶠ (x : α) in pure a, p x) ↔ p a

@[simp]

theorem Filter.principal_singleton {α : Type u} (a : α) : Filter.principal {a} = pure a

@[simp]

theorem Filter.map_pure {α : Type u} {β : Type v} (f : α → β) (a : α) : Filter.map f (pure a) = pure (f a)

theorem Filter.pure_le_principal {α : Type u} {s : Set α} (a : α) : pure a ≤ Filter.principal s ↔ a ∈ s

@[simp]

theorem Filter.join_pure {α : Type u} (f : Filter α) : (pure f).join = f

@[simp]

theorem Filter.pure_bind {α : Type u} {β : Type v} (a : α) (m : α → Filter β) : (pure a).bind m = m a

theorem Filter.map_bind {γ : Type w} {α : Type u_2} {β : Type u_3} (m : β → γ) (f : Filter α) (g : α → Filter β) : Filter.map m (f.bind g) = f.bind (Filter.map m ∘ g)

theorem Filter.bind_map {γ : Type w} {α : Type u_2} {β : Type u_3} (m : α → β) (f : Filter α) (g : β → Filter γ) : (Filter.map m f).bind g = f.bind (g ∘ m)

Filter as a Monad

In this section we define Filter.monad, a Monad structure on Filters. This definition is not an instance because its Seq projection is not equal to the Filter.seq function we use in the Applicative instance on Filter.

def Filter.monad : Monad Filter

The monad structure on filters.

Equations

• Filter.monad = Monad.mk

theorem Filter.lawfulMonad : LawfulMonad Filter

instance Filter.instAlternative : Alternative Filter

Equations

• Filter.instAlternative = Alternative.mk (fun {α : Type u_2} => ⊥) fun {α : Type u_2} (x : Filter α) (y : Unit → Filter α) => x ⊔ y ()

@[simp]

theorem Filter.map_def {α : Type u_2} {β : Type u_2} (m : α → β) (f : Filter α) : m <$> f = Filter.map m f

@[simp]

theorem Filter.bind_def {α : Type u_2} {β : Type u_2} (f : Filter α) (m : α → Filter β) : f >>= m = f.bind m

map and comap equations

@[simp]

theorem Filter.mem_comap {α : Type u} {β : Type v} {g : Filter β} {m : α → β} {s : Set α} : s ∈ Filter.comap m g ↔ ∃ t ∈ g, m ⁻¹' t ⊆ s

theorem Filter.preimage_mem_comap {α : Type u} {β : Type v} {g : Filter β} {m : α → β} {t : Set β} (ht : t ∈ g) : m ⁻¹' t ∈ Filter.comap m g

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)

theorem Filter.comap_id {α : Type u} {f : Filter α} : Filter.comap id f = f

theorem Filter.comap_id' {α : Type u} {f : Filter α} : Filter.comap (fun (x : α) => x) f = f

theorem Filter.comap_const_of_not_mem {α : Type u} {β : Type v} {g : Filter β} {t : Set β} {x : β} (ht : t ∈ g) (hx : x ∉ t) : Filter.comap (fun (x_1 : α) => x) g = ⊥

theorem Filter.comap_const_of_mem {α : Type u} {β : Type v} {g : Filter β} {x : β} (h : ∀ t ∈ g, x ∈ t) : Filter.comap (fun (x_1 : α) => x) g = ⊤

theorem Filter.map_const {α : Type u} {β : Type v} {f : Filter α} [f.NeBot] {c : β} : Filter.map (fun (x : α) => c) f = pure c

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:

    φ
  α → β
θ ↓   ↓ ψ
  γ → δ
    ρ

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)

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)

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)

theorem Function.Commute.filter_map {α : Type u} {f : α → α} {g : α → α} (h : Function.Commute f g) : Function.Commute (Filter.map f) (Filter.map g)

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)

theorem Function.Commute.filter_comap {α : Type u} {f : α → α} {g : α → α} (h : Function.Commute f g) : Function.Commute (Filter.comap f) (Filter.comap g)

theorem Function.LeftInverse.filter_map {α : Type u} {β : Type v} {f : α → β} {g : β → α} (hfg : Function.LeftInverse g f) : Function.LeftInverse (Filter.map g) (Filter.map f)

theorem Function.LeftInverse.filter_comap {α : Type u} {β : Type v} {f : α → β} {g : β → α} (hfg : Function.LeftInverse g f) : Function.RightInverse (Filter.comap g) (Filter.comap f)

theorem Function.RightInverse.filter_map {α : Type u} {β : Type v} {f : α → β} {g : β → α} (hfg : Function.RightInverse g f) : Function.RightInverse (Filter.map g) (Filter.map f)

theorem Function.RightInverse.filter_comap {α : Type u} {β : Type v} {f : α → β} {g : β → α} (hfg : Function.RightInverse g f) : Function.LeftInverse (Filter.comap g) (Filter.comap f)

theorem Set.LeftInvOn.filter_map_Iic {α : Type u} {β : Type v} {s : Set α} {f : α → β} {g : β → α} (hfg : Set.LeftInvOn g f s) : Set.LeftInvOn (Filter.map g) (Filter.map f) (Set.Iic (Filter.principal s))

theorem Set.RightInvOn.filter_map_Iic {α : Type u} {β : Type v} {t : Set β} {f : α → β} {g : β → α} (hfg : Set.RightInvOn g f t) : Set.RightInvOn (Filter.map g) (Filter.map f) (Set.Iic (Filter.principal t))

@[simp]

theorem Filter.comap_principal {α : Type u} {β : Type v} {m : α → β} {t : Set β} : Filter.comap m (Filter.principal t) = Filter.principal (m ⁻¹' t)

theorem Filter.principal_subtype {α : Type u_2} (s : Set α) (t : Set ↑s) : Filter.principal t = Filter.comap Subtype.val (Filter.principal (Subtype.val '' t))

@[simp]

theorem Filter.comap_pure {α : Type u} {β : Type v} {m : α → β} {b : β} : Filter.comap m (pure b) = Filter.principal (m ⁻¹' {b})

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

theorem Filter.gc_map_comap {α : Type u} {β : Type v} (m : α → β) : GaloisConnection (Filter.map m) (Filter.comap m)

theorem Filter.comap_le_iff_le_kernMap {α : Type u} {β : Type v} {f : Filter α} {g : Filter β} {m : α → β} : Filter.comap m g ≤ f ↔ g ≤ Filter.kernMap m f

theorem Filter.gc_comap_kernMap {α : Type u} {β : Type v} (m : α → β) : GaloisConnection (Filter.comap m) (Filter.kernMap m)

theorem Filter.kernMap_principal {α : Type u} {β : Type v} {m : α → β} {s : Set α} : Filter.kernMap m (Filter.principal s) = Filter.principal (Set.kernImage m s)

theorem Filter.map_mono {α : Type u} {β : Type v} {m : α → β} : Monotone (Filter.map m)

theorem Filter.comap_mono {α : Type u} {β : Type v} {m : α → β} : Monotone (Filter.comap m)

theorem GCongr.Filter.map_le_map {α : Type u} {β : Type v} {m : α → β} {F : Filter α} {G : Filter α} (h : F ≤ G) : Filter.map m F ≤ Filter.map m G

Temporary lemma that we can tag with gcongr

theorem GCongr.Filter.comap_le_comap {α : Type u} {β : Type v} {m : α → β} {F : Filter β} {G : Filter β} (h : F ≤ G) : Filter.comap m F ≤ Filter.comap m G

Temporary lemma that we can tag with gcongr

@[simp]

theorem Filter.map_bot {α : Type u} {β : Type v} {m : α → β} : Filter.map m ⊥ = ⊥

@[simp]

theorem Filter.map_sup {α : Type u} {β : Type v} {f₁ : Filter α} {f₂ : Filter α} {m : α → β} : Filter.map m (f₁ ⊔ f₂) = Filter.map m f₁ ⊔ Filter.map m f₂

@[simp]

theorem Filter.map_iSup {α : Type u} {β : Type v} {ι : Sort x} {m : α → β} {f : ι → Filter α} : Filter.map m (⨆ (i : ι), f i) = ⨆ (i : ι), Filter.map m (f i)

@[simp]

theorem Filter.map_top {α : Type u} {β : Type v} (f : α → β) : Filter.map f ⊤ = Filter.principal (Set.range f)

@[simp]

theorem Filter.comap_top {α : Type u} {β : Type v} {m : α → β} : Filter.comap m ⊤ = ⊤

@[simp]

theorem Filter.comap_inf {α : Type u} {β : Type v} {g₁ : Filter β} {g₂ : Filter β} {m : α → β} : Filter.comap m (g₁ ⊓ g₂) = Filter.comap m g₁ ⊓ Filter.comap m g₂

@[simp]

theorem Filter.comap_iInf {α : Type u} {β : Type v} {ι : Sort x} {m : α → β} {f : ι → Filter β} : Filter.comap m (⨅ (i : ι), f i) = ⨅ (i : ι), Filter.comap m (f i)

theorem Filter.le_comap_top {α : Type u} {β : Type v} (f : α → β) (l : Filter α) : l ≤ Filter.comap f ⊤

theorem Filter.map_comap_le {α : Type u} {β : Type v} {g : Filter β} {m : α → β} : Filter.map m (Filter.comap m g) ≤ g

theorem Filter.le_comap_map {α : Type u} {β : Type v} {f : Filter α} {m : α → β} : f ≤ Filter.comap m (Filter.map m f)

@[simp]

theorem Filter.comap_bot {α : Type u} {β : Type v} {m : α → β} : Filter.comap m ⊥ = ⊥

theorem Filter.neBot_of_comap {α : Type u} {β : Type v} {g : Filter β} {m : α → β} (h : (Filter.comap m g).NeBot) : g.NeBot

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

theorem Filter.disjoint_comap {α : Type u} {β : Type v} {g₁ : Filter β} {g₂ : Filter β} {m : α → β} (h : Disjoint g₁ g₂) : Disjoint (Filter.comap m g₁) (Filter.comap m g₂)

theorem Filter.comap_iSup {α : Type u} {β : Type v} {ι : Sort u_2} {f : ι → Filter β} {m : α → β} : Filter.comap m (iSup f) = ⨆ (i : ι), Filter.comap m (f i)

theorem Filter.comap_sSup {α : Type u} {β : Type v} {s : Set (Filter β)} {m : α → β} : Filter.comap m (sSup s) = ⨆ f ∈ s, Filter.comap m f

theorem Filter.comap_sup {α : Type u} {β : Type v} {g₁ : Filter β} {g₂ : Filter β} {m : α → β} : Filter.comap m (g₁ ⊔ g₂) = Filter.comap m g₁ ⊔ Filter.comap m g₂

theorem Filter.map_comap {α : Type u} {β : Type v} (f : Filter β) (m : α → β) : Filter.map m (Filter.comap m f) = f ⊓ Filter.principal (Set.range m)

theorem Filter.map_comap_setCoe_val {β : Type v} (f : Filter β) (s : Set β) : Filter.map Subtype.val (Filter.comap Subtype.val f) = f ⊓ Filter.principal s

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

instance Filter.canLift {α : Type u} {β : Type v} (c : β → α) (p : α → Prop) [CanLift α β c p] : CanLift (Filter α) (Filter β) (Filter.map c) fun (f : Filter α) => ∀ᶠ (x : α) in f, p x

Equations

• ⋯ = ⋯

theorem Filter.comap_le_comap_iff {α : Type u} {β : Type v} {f : Filter β} {g : Filter β} {m : α → β} (hf : Set.range m ∈ f) : Filter.comap m f ≤ Filter.comap m g ↔ f ≤ g

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

theorem Filter.comap_injective {α : Type u} {β : Type v} {f : α → β} (hf : Function.Surjective f) : Function.Injective (Filter.comap f)

theorem Function.Surjective.filter_map_top {α : Type u} {β : Type v} {f : α → β} (hf : Function.Surjective f) : Filter.map f ⊤ = ⊤

theorem Filter.subtype_coe_map_comap {α : Type u} (s : Set α) (f : Filter α) : Filter.map Subtype.val (Filter.comap Subtype.val f) = f ⊓ Filter.principal s

theorem Filter.image_mem_of_mem_comap {α : Type u} {β : Type v} {f : Filter α} {c : β → α} (h : Set.range c ∈ f) {W : Set β} (W_in : W ∈ Filter.comap c f) : c '' W ∈ f

theorem Filter.image_coe_mem_of_mem_comap {α : Type u} {f : Filter α} {U : Set α} (h : U ∈ f) {W : Set ↑U} (W_in : W ∈ Filter.comap Subtype.val f) : Subtype.val '' W ∈ f

theorem Filter.comap_map {α : Type u} {β : Type v} {f : Filter α} {m : α → β} (h : Function.Injective m) : Filter.comap m (Filter.map m f) = f

theorem Filter.mem_comap_iff {α : Type u} {β : Type v} {f : Filter β} {m : α → β} (inj : Function.Injective m) (large : Set.range m ∈ f) {S : Set α} : S ∈ Filter.comap m f ↔ m '' S ∈ f

theorem Filter.map_le_map_iff_of_injOn {α : Type u} {β : Type v} {l₁ : Filter α} {l₂ : Filter α} {f : α → β} {s : Set α} (h₁ : s ∈ l₁) (h₂ : s ∈ l₂) (hinj : Set.InjOn f s) : Filter.map f l₁ ≤ Filter.map f l₂ ↔ l₁ ≤ l₂

theorem Filter.map_le_map_iff {α : Type u} {β : Type v} {f : Filter α} {g : Filter α} {m : α → β} (hm : Function.Injective m) : Filter.map m f ≤ Filter.map m g ↔ f ≤ g

theorem Filter.map_eq_map_iff_of_injOn {α : Type u} {β : Type v} {f : Filter α} {g : Filter α} {m : α → β} {s : Set α} (hsf : s ∈ f) (hsg : s ∈ g) (hm : Set.InjOn m s) : Filter.map m f = Filter.map m g ↔ f = g

theorem Filter.map_inj {α : Type u} {β : Type v} {f : Filter α} {g : Filter α} {m : α → β} (hm : Function.Injective m) : Filter.map m f = Filter.map m g ↔ f = g

theorem Filter.map_injective {α : Type u} {β : Type v} {m : α → β} (hm : Function.Injective m) : Function.Injective (Filter.map m)

theorem Filter.comap_neBot_iff {α : Type u} {β : Type v} {f : Filter β} {m : α → β} : (Filter.comap m f).NeBot ↔ ∀ t ∈ f, ∃ (a : α), m a ∈ t

theorem Filter.comap_neBot {α : Type u} {β : Type v} {f : Filter β} {m : α → β} (hm : ∀ t ∈ f, ∃ (a : α), m a ∈ t) : (Filter.comap m f).NeBot

theorem Filter.comap_neBot_iff_frequently {α : Type u} {β : Type v} {f : Filter β} {m : α → β} : (Filter.comap m f).NeBot ↔ ∃ᶠ (y : β) in f, y ∈ Set.range m

theorem Filter.comap_neBot_iff_compl_range {α : Type u} {β : Type v} {f : Filter β} {m : α → β} : (Filter.comap m f).NeBot ↔ (Set.range m)ᶜ ∉ f

theorem Filter.comap_eq_bot_iff_compl_range {α : Type u} {β : Type v} {f : Filter β} {m : α → β} : Filter.comap m f = ⊥ ↔ (Set.range m)ᶜ ∈ f

theorem Filter.comap_surjective_eq_bot {α : Type u} {β : Type v} {f : Filter β} {m : α → β} (hm : Function.Surjective m) : Filter.comap m f = ⊥ ↔ f = ⊥

theorem Filter.disjoint_comap_iff {α : Type u} {β : Type v} {g₁ : Filter β} {g₂ : Filter β} {m : α → β} (h : Function.Surjective m) : Disjoint (Filter.comap m g₁) (Filter.comap m g₂) ↔ Disjoint g₁ g₂

theorem Filter.NeBot.comap_of_range_mem {α : Type u} {β : Type v} {f : Filter β} {m : α → β} : f.NeBot → Set.range m ∈ f → (Filter.comap m f).NeBot

@[simp]

theorem Filter.comap_fst_neBot_iff {α : Type u} {β : Type v} {f : Filter α} : (Filter.comap Prod.fst f).NeBot ↔ f.NeBot ∧ Nonempty β

theorem Filter.comap_fst_neBot {α : Type u} {β : Type v} [Nonempty β] {f : Filter α} [f.NeBot] : (Filter.comap Prod.fst f).NeBot

@[simp]

theorem Filter.comap_snd_neBot_iff {α : Type u} {β : Type v} {f : Filter β} : (Filter.comap Prod.snd f).NeBot ↔ Nonempty α ∧ f.NeBot

theorem Filter.comap_snd_neBot {α : Type u} {β : Type v} [Nonempty α] {f : Filter β} [f.NeBot] : (Filter.comap Prod.snd f).NeBot

theorem Filter.comap_eval_neBot_iff' {ι : Type u_2} {α : ι → Type u_3} {i : ι} {f : Filter (α i)} : (Filter.comap (Function.eval i) f).NeBot ↔ (∀ (j : ι), Nonempty (α j)) ∧ f.NeBot

@[simp]

theorem Filter.comap_eval_neBot_iff {ι : Type u_2} {α : ι → Type u_3} [∀ (j : ι), Nonempty (α j)] {i : ι} {f : Filter (α i)} : (Filter.comap (Function.eval i) f).NeBot ↔ f.NeBot

theorem Filter.comap_eval_neBot {ι : Type u_2} {α : ι → Type u_3} [∀ (j : ι), Nonempty (α j)] (i : ι) (f : Filter (α i)) [f.NeBot] : (Filter.comap (Function.eval i) f).NeBot

theorem Filter.comap_inf_principal_neBot_of_image_mem {α : Type u} {β : Type v} {f : Filter β} {m : α → β} (hf : f.NeBot) {s : Set α} (hs : m '' s ∈ f) : (Filter.comap m f ⊓ Filter.principal s).NeBot

theorem Filter.comap_coe_neBot_of_le_principal {γ : Type w} {s : Set γ} {l : Filter γ} [h : l.NeBot] (h' : l ≤ Filter.principal s) : (Filter.comap Subtype.val l).NeBot

theorem Filter.NeBot.comap_of_surj {α : Type u} {β : Type v} {f : Filter β} {m : α → β} (hf : f.NeBot) (hm : Function.Surjective m) : (Filter.comap m f).NeBot

theorem Filter.NeBot.comap_of_image_mem {α : Type u} {β : Type v} {f : Filter β} {m : α → β} (hf : f.NeBot) {s : Set α} (hs : m '' s ∈ f) : (Filter.comap m f).NeBot

@[simp]

theorem Filter.map_eq_bot_iff {α : Type u} {β : Type v} {f : Filter α} {m : α → β} : Filter.map m f = ⊥ ↔ f = ⊥

theorem Filter.map_neBot_iff {α : Type u} {β : Type v} (f : α → β) {F : Filter α} : (Filter.map f F).NeBot ↔ F.NeBot

theorem Filter.NeBot.map {α : Type u} {β : Type v} {f : Filter α} (hf : f.NeBot) (m : α → β) : (Filter.map m f).NeBot

theorem Filter.NeBot.of_map {α : Type u} {β : Type v} {f : Filter α} {m : α → β} : (Filter.map m f).NeBot → f.NeBot

instance Filter.map_neBot {α : Type u} {β : Type v} {f : Filter α} {m : α → β} [hf : f.NeBot] : (Filter.map m f).NeBot

Equations

• ⋯ = ⋯

theorem Filter.sInter_comap_sets {α : Type u} {β : Type v} (f : α → β) (F : Filter β) : ⋂₀ (Filter.comap f F).sets = ⋂ U ∈ F, f ⁻¹' U

theorem Filter.map_iInf_le {α : Type u} {β : Type v} {ι : Sort x} {f : ι → Filter α} {m : α → β} : Filter.map m (iInf f) ≤ ⨅ (i : ι), Filter.map m (f i)

theorem Filter.map_iInf_eq {α : Type u} {β : Type v} {ι : Sort x} {f : ι → Filter α} {m : α → β} (hf : Directed (fun (x x_1 : Filter α) => x ≥ x_1) f) [Nonempty ι] : Filter.map m (iInf f) = ⨅ (i : ι), Filter.map m (f i)

theorem Filter.map_biInf_eq {α : Type u} {β : Type v} {ι : Type w} {f : ι → Filter α} {m : α → β} {p : ι → Prop} (h : DirectedOn (f ⁻¹'o fun (x x_1 : Filter α) => x ≥ x_1) {x : ι | p x}) (ne : ∃ (i : ι), p i) : Filter.map m (⨅ (i : ι), ⨅ (_ : p i), f i) = ⨅ (i : ι), ⨅ (_ : p i), Filter.map m (f i)

theorem Filter.map_inf_le {α : Type u} {β : Type v} {f : Filter α} {g : Filter α} {m : α → β} : Filter.map m (f ⊓ g) ≤ Filter.map m f ⊓ Filter.map m g

theorem Filter.map_inf {α : Type u} {β : Type v} {f : Filter α} {g : Filter α} {m : α → β} (h : Function.Injective m) : Filter.map m (f ⊓ g) = Filter.map m f ⊓ Filter.map m g

theorem Filter.map_inf' {α : Type u} {β : Type v} {f : Filter α} {g : Filter α} {m : α → β} {t : Set α} (htf : t ∈ f) (htg : t ∈ g) (h : Set.InjOn m t) : Filter.map m (f ⊓ g) = Filter.map m f ⊓ Filter.map m g

theorem Filter.disjoint_of_map {α : Type u_2} {β : Type u_3} {F : Filter α} {G : Filter α} {f : α → β} (h : Disjoint (Filter.map f F) (Filter.map f G)) : Disjoint F G

theorem Filter.disjoint_map {α : Type u} {β : Type v} {m : α → β} (hm : Function.Injective m) {f₁ : Filter α} {f₂ : Filter α} : Disjoint (Filter.map m f₁) (Filter.map m f₂) ↔ Disjoint f₁ f₂

theorem Filter.map_equiv_symm {α : Type u} {β : Type v} (e : α ≃ β) (f : Filter β) : Filter.map (⇑e.symm) f = Filter.comap (⇑e) f

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

theorem Filter.comap_equiv_symm {α : Type u} {β : Type v} (e : α ≃ β) (f : Filter α) : Filter.comap (⇑e.symm) f = Filter.map (⇑e) f

theorem Filter.map_swap_eq_comap_swap {α : Type u} {β : Type v} {f : Filter (α × β)} : Prod.swap <$> f = Filter.comap Prod.swap f

theorem Filter.map_swap4_eq_comap {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} {f : Filter ((α × β) × γ × δ)} : Filter.map (fun (p : (α × β) × γ × δ) => ((p.1.1, p.2.1), p.1.2, p.2.2)) f = Filter.comap (fun (p : (α × γ) × β × δ) => ((p.1.1, p.2.1), p.1.2, p.2.2)) f

A useful lemma when dealing with uniformities.

theorem Filter.le_map {α : Type u} {β : Type v} {f : Filter α} {m : α → β} {g : Filter β} (h : ∀ s ∈ f, m '' s ∈ g) : g ≤ Filter.map m f

theorem Filter.le_map_iff {α : Type u} {β : Type v} {f : Filter α} {m : α → β} {g : Filter β} : g ≤ Filter.map m f ↔ ∀ s ∈ f, m '' s ∈ g

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

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

theorem Filter.principal_eq_map_coe_top {α : Type u} (s : Set α) : Filter.principal s = Filter.map Subtype.val ⊤

theorem Filter.inf_principal_eq_bot_iff_comap {α : Type u} {F : Filter α} {s : Set α} : F ⊓ Filter.principal s = ⊥ ↔ Filter.comap Subtype.val F = ⊥

theorem Filter.singleton_mem_pure {α : Type u} {a : α} : {a} ∈ pure a

theorem Filter.pure_injective {α : Type u} : Function.Injective pure

instance Filter.pure_neBot {α : Type u} {a : α} : (pure a).NeBot

Equations

• ⋯ = ⋯

@[simp]

theorem Filter.le_pure_iff {α : Type u} {f : Filter α} {a : α} : f ≤ pure a ↔ {a} ∈ f

theorem Filter.mem_seq_def {α : Type u} {β : Type v} {f : Filter (α → β)} {g : Filter α} {s : Set β} : s ∈ f.seq g ↔ ∃ u ∈ f, ∃ t ∈ g, ∀ x ∈ u, ∀ y ∈ t, x y ∈ s

theorem Filter.mem_seq_iff {α : Type u} {β : Type v} {f : Filter (α → β)} {g : Filter α} {s : Set β} : s ∈ f.seq g ↔ ∃ u ∈ f, ∃ t ∈ g, u.seq t ⊆ s

theorem Filter.mem_map_seq_iff {α : Type u} {β : Type v} {γ : Type w} {f : Filter α} {g : Filter β} {m : α → β → γ} {s : Set γ} : s ∈ (Filter.map m f).seq g ↔ ∃ (t : Set β) (u : Set α), t ∈ g ∧ u ∈ f ∧ ∀ x ∈ u, ∀ y ∈ t, m x y ∈ s

theorem Filter.seq_mem_seq {α : Type u} {β : Type v} {f : Filter (α → β)} {g : Filter α} {s : Set (α → β)} {t : Set α} (hs : s ∈ f) (ht : t ∈ g) : s.seq t ∈ f.seq g

theorem Filter.le_seq {α : Type u} {β : Type v} {f : Filter (α → β)} {g : Filter α} {h : Filter β} (hh : ∀ t ∈ f, ∀ u ∈ g, t.seq u ∈ h) : h ≤ f.seq g

theorem Filter.seq_mono {α : Type u} {β : Type v} {f₁ : Filter (α → β)} {f₂ : Filter (α → β)} {g₁ : Filter α} {g₂ : Filter α} (hf : f₁ ≤ f₂) (hg : g₁ ≤ g₂) : f₁.seq g₁ ≤ f₂.seq g₂

@[simp]

theorem Filter.pure_seq_eq_map {α : Type u} {β : Type v} (g : α → β) (f : Filter α) : (pure g).seq f = Filter.map g f

@[simp]

theorem Filter.seq_pure {α : Type u} {β : Type v} (f : Filter (α → β)) (a : α) : f.seq (pure a) = Filter.map (fun (g : α → β) => g a) f

@[simp]

theorem Filter.seq_assoc {α : Type u} {β : Type v} {γ : Type w} (x : Filter α) (g : Filter (α → β)) (h : Filter (β → γ)) : h.seq (g.seq x) = ((Filter.map (fun (x : β → γ) (x_1 : α → β) => x ∘ x_1) h).seq g).seq x

theorem Filter.prod_map_seq_comm {α : Type u} {β : Type v} (f : Filter α) (g : Filter β) : (Filter.map Prod.mk f).seq g = (Filter.map (fun (b : β) (a : α) => (a, b)) g).seq f

theorem Filter.seq_eq_filter_seq {α : Type u} {β : Type u} (f : Filter (α → β)) (g : Filter α) : (Seq.seq f fun (x : Unit) => g) = f.seq g

instance Filter.instLawfulApplicative : LawfulApplicative Filter

Equations

• Filter.instLawfulApplicative = ⋯

instance Filter.instCommApplicative : CommApplicative Filter

Equations

• Filter.instCommApplicative = ⋯

bind equations

@[simp]

theorem Filter.eventually_bind {α : Type u} {β : Type v} {f : Filter α} {m : α → Filter β} {p : β → Prop} : (∀ᶠ (y : β) in f.bind m, p y) ↔ ∀ᶠ (x : α) in f, ∀ᶠ (y : β) in m x, p y

@[simp]

theorem Filter.eventuallyEq_bind {α : Type u} {β : Type v} {γ : Type w} {f : Filter α} {m : α → Filter β} {g₁ : β → γ} {g₂ : β → γ} : g₁ =ᶠ[f.bind m] g₂ ↔ ∀ᶠ (x : α) in f, g₁ =ᶠ[m x] g₂

@[simp]

theorem Filter.eventuallyLE_bind {α : Type u} {β : Type v} {γ : Type w} [LE γ] {f : Filter α} {m : α → Filter β} {g₁ : β → γ} {g₂ : β → γ} : g₁ ≤ᶠ[f.bind m] g₂ ↔ ∀ᶠ (x : α) in f, g₁ ≤ᶠ[m x] g₂

theorem Filter.mem_bind' {α : Type u} {β : Type v} {s : Set β} {f : Filter α} {m : α → Filter β} : s ∈ f.bind m ↔ {a : α | s ∈ m a} ∈ f

@[simp]

theorem Filter.mem_bind {α : Type u} {β : Type v} {s : Set β} {f : Filter α} {m : α → Filter β} : s ∈ f.bind m ↔ ∃ t ∈ f, ∀ x ∈ t, s ∈ m x

theorem Filter.bind_le {α : Type u} {β : Type v} {f : Filter α} {g : α → Filter β} {l : Filter β} (h : ∀ᶠ (x : α) in f, g x ≤ l) : f.bind g ≤ l

theorem Filter.bind_mono {α : Type u} {β : Type v} {f₁ : Filter α} {f₂ : Filter α} {g₁ : α → Filter β} {g₂ : α → Filter β} (hf : f₁ ≤ f₂) (hg : g₁ ≤ᶠ[f₁] g₂) : f₁.bind g₁ ≤ f₂.bind g₂

theorem Filter.bind_inf_principal {α : Type u} {β : Type v} {f : Filter α} {g : α → Filter β} {s : Set β} : (f.bind fun (x : α) => g x ⊓ Filter.principal s) = f.bind g ⊓ Filter.principal s

theorem Filter.sup_bind {α : Type u} {β : Type v} {f : Filter α} {g : Filter α} {h : α → Filter β} : (f ⊔ g).bind h = f.bind h ⊔ g.bind h

theorem Filter.principal_bind {α : Type u} {β : Type v} {s : Set α} {f : α → Filter β} : (Filter.principal s).bind f = ⨆ x ∈ s, f x

Limits

def Filter.Tendsto {α : Type u} {β : Type v} (f : α → β) (l₁ : Filter α) (l₂ : Filter β) : Prop

Filter.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₂)

theorem Filter.tendsto_def {α : Type u} {β : Type v} {f : α → β} {l₁ : Filter α} {l₂ : Filter β} : Filter.Tendsto f l₁ l₂ ↔ ∀ s ∈ l₂, f ⁻¹' s ∈ l₁

theorem Filter.tendsto_iff_eventually {α : Type u} {β : Type v} {f : α → β} {l₁ : Filter α} {l₂ : Filter β} : Filter.Tendsto f l₁ l₂ ↔ ∀ ⦃p : β → Prop⦄, (∀ᶠ (y : β) in l₂, p y) → ∀ᶠ (x : α) in l₁, p (f x)

theorem Filter.tendsto_iff_forall_eventually_mem {α : Type u} {β : Type v} {f : α → β} {l₁ : Filter α} {l₂ : Filter β} : Filter.Tendsto f l₁ l₂ ↔ ∀ s ∈ l₂, ∀ᶠ (x : α) in l₁, f x ∈ s

theorem Filter.Tendsto.eventually_mem {α : Type u} {β : Type v} {f : α → β} {l₁ : Filter α} {l₂ : Filter β} {s : Set β} (hf : Filter.Tendsto f l₁ l₂) (h : s ∈ l₂) : ∀ᶠ (x : α) in l₁, f x ∈ s

theorem Filter.Tendsto.eventually {α : Type u} {β : Type v} {f : α → β} {l₁ : Filter α} {l₂ : Filter β} {p : β → Prop} (hf : Filter.Tendsto f l₁ l₂) (h : ∀ᶠ (y : β) in l₂, p y) : ∀ᶠ (x : α) in l₁, p (f x)

theorem Filter.not_tendsto_iff_exists_frequently_nmem {α : Type u} {β : Type v} {f : α → β} {l₁ : Filter α} {l₂ : Filter β} : ¬Filter.Tendsto f l₁ l₂ ↔ ∃ s ∈ l₂, ∃ᶠ (x : α) in l₁, f x ∉ s

theorem Filter.Tendsto.frequently {α : Type u} {β : Type v} {f : α → β} {l₁ : Filter α} {l₂ : Filter β} {p : β → Prop} (hf : Filter.Tendsto f l₁ l₂) (h : ∃ᶠ (x : α) in l₁, p (f x)) : ∃ᶠ (y : β) in l₂, p y

theorem Filter.Tendsto.frequently_map {α : Type u} {β : Type v} {l₁ : Filter α} {l₂ : Filter β} {p : α → Prop} {q : β → Prop} (f : α → β) (c : Filter.Tendsto f l₁ l₂) (w : ∀ (x : α), p x → q (f x)) (h : ∃ᶠ (x : α) in l₁, p x) : ∃ᶠ (y : β) in l₂, q y

@[simp]

theorem Filter.tendsto_bot {α : Type u} {β : Type v} {f : α → β} {l : Filter β} : Filter.Tendsto f ⊥ l

@[simp]

theorem Filter.tendsto_top {α : Type u} {β : Type v} {f : α → β} {l : Filter α} : Filter.Tendsto f l ⊤

theorem Filter.le_map_of_right_inverse {α : Type u} {β : Type v} {mab : α → β} {mba : β → α} {f : Filter α} {g : Filter β} (h₁ : mab ∘ mba =ᶠ[g] id) (h₂ : Filter.Tendsto mba g f) : g ≤ Filter.map mab f

theorem Filter.tendsto_of_isEmpty {α : Type u} {β : Type v} [IsEmpty α] {f : α → β} {la : Filter α} {lb : Filter β} : Filter.Tendsto f la lb

theorem Filter.eventuallyEq_of_left_inv_of_right_inv {α : Type u} {β : Type v} {f : α → β} {g₁ : β → α} {g₂ : β → α} {fa : Filter α} {fb : Filter β} (hleft : ∀ᶠ (x : α) in fa, g₁ (f x) = x) (hright : ∀ᶠ (y : β) in fb, f (g₂ y) = y) (htendsto : Filter.Tendsto g₂ fb fa) : g₁ =ᶠ[fb] g₂

theorem Filter.tendsto_iff_comap {α : Type u} {β : Type v} {f : α → β} {l₁ : Filter α} {l₂ : Filter β} : Filter.Tendsto f l₁ l₂ ↔ l₁ ≤ Filter.comap f l₂

theorem Filter.Tendsto.le_comap {α : Type u} {β : Type v} {f : α → β} {l₁ : Filter α} {l₂ : Filter β} : Filter.Tendsto f l₁ l₂ → l₁ ≤ Filter.comap f l₂

Alias of the forward direction of Filter.tendsto_iff_comap.

theorem Filter.Tendsto.disjoint {α : Type u} {β : Type v} {f : α → β} {la₁ : Filter α} {la₂ : Filter α} {lb₁ : Filter β} {lb₂ : Filter β} (h₁ : Filter.Tendsto f la₁ lb₁) (hd : Disjoint lb₁ lb₂) (h₂ : Filter.Tendsto f la₂ lb₂) : Disjoint la₁ la₂

theorem Filter.tendsto_congr' {α : Type u} {β : Type v} {f₁ : α → β} {f₂ : α → β} {l₁ : Filter α} {l₂ : Filter β} (hl : f₁ =ᶠ[l₁] f₂) : Filter.Tendsto f₁ l₁ l₂ ↔ Filter.Tendsto f₂ l₁ l₂

theorem Filter.Tendsto.congr' {α : Type u} {β : Type v} {f₁ : α → β} {f₂ : α → β} {l₁ : Filter α} {l₂ : Filter β} (hl : f₁ =ᶠ[l₁] f₂) (h : Filter.Tendsto f₁ l₁ l₂) : Filter.Tendsto f₂ l₁ l₂

theorem Filter.tendsto_congr {α : Type u} {β : Type v} {f₁ : α → β} {f₂ : α → β} {l₁ : Filter α} {l₂ : Filter β} (h : ∀ (x : α), f₁ x = f₂ x) : Filter.Tendsto f₁ l₁ l₂ ↔ Filter.Tendsto f₂ l₁ l₂

theorem Filter.Tendsto.congr {α : Type u} {β : Type v} {f₁ : α → β} {f₂ : α → β} {l₁ : Filter α} {l₂ : Filter β} (h : ∀ (x : α), f₁ x = f₂ x) : Filter.Tendsto f₁ l₁ l₂ → Filter.Tendsto f₂ l₁ l₂

theorem Filter.tendsto_id' {α : Type u} {x : Filter α} {y : Filter α} : Filter.Tendsto id x y ↔ x ≤ y

theorem Filter.tendsto_id {α : Type u} {x : Filter α} : Filter.Tendsto id x x

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

theorem Filter.Tendsto.iterate {α : Type u} {f : α → α} {l : Filter α} (h : Filter.Tendsto f l l) (n : ℕ) : Filter.Tendsto f^[n] l l

theorem Filter.Tendsto.mono_left {α : Type u} {β : Type v} {f : α → β} {x : Filter α} {y : Filter α} {z : Filter β} (hx : Filter.Tendsto f x z) (h : y ≤ x) : Filter.Tendsto f y z

theorem Filter.Tendsto.mono_right {α : Type u} {β : Type v} {f : α → β} {x : Filter α} {y : Filter β} {z : Filter β} (hy : Filter.Tendsto f x y) (hz : y ≤ z) : Filter.Tendsto f x z

theorem Filter.Tendsto.neBot {α : Type u} {β : Type v} {f : α → β} {x : Filter α} {y : Filter β} (h : Filter.Tendsto f x y) [hx : x.NeBot] : y.NeBot

theorem Filter.tendsto_map {α : Type u} {β : Type v} {f : α → β} {x : Filter α} : Filter.Tendsto f x (Filter.map f x)

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

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

Alias of the reverse direction of Filter.tendsto_map'_iff.

theorem Filter.tendsto_comap {α : Type u} {β : Type v} {f : α → β} {x : Filter β} : Filter.Tendsto f (Filter.comap f x) x

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

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

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

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

theorem Filter.map_eq_of_inverse {α : Type u} {β : Type v} {f : Filter α} {g : Filter β} {φ : α → β} (ψ : β → α) (eq : φ ∘ ψ = id) (hφ : Filter.Tendsto φ f g) (hψ : Filter.Tendsto ψ g f) : Filter.map φ f = g

theorem Filter.tendsto_inf {α : Type u} {β : Type v} {f : α → β} {x : Filter α} {y₁ : Filter β} {y₂ : Filter β} : Filter.Tendsto f x (y₁ ⊓ y₂) ↔ Filter.Tendsto f x y₁ ∧ Filter.Tendsto f x y₂

theorem Filter.tendsto_inf_left {α : Type u} {β : Type v} {f : α → β} {x₁ : Filter α} {x₂ : Filter α} {y : Filter β} (h : Filter.Tendsto f x₁ y) : Filter.Tendsto f (x₁ ⊓ x₂) y

theorem Filter.tendsto_inf_right {α : Type u} {β : Type v} {f : α → β} {x₁ : Filter α} {x₂ : Filter α} {y : Filter β} (h : Filter.Tendsto f x₂ y) : Filter.Tendsto f (x₁ ⊓ x₂) y

theorem Filter.Tendsto.inf {α : Type u} {β : Type v} {f : α → β} {x₁ : Filter α} {x₂ : Filter α} {y₁ : Filter β} {y₂ : Filter β} (h₁ : Filter.Tendsto f x₁ y₁) (h₂ : Filter.Tendsto f x₂ y₂) : Filter.Tendsto f (x₁ ⊓ x₂) (y₁ ⊓ y₂)

@[simp]

theorem Filter.tendsto_iInf {α : Type u} {β : Type v} {ι : Sort x} {f : α → β} {x : Filter α} {y : ι → Filter β} : Filter.Tendsto f x (⨅ (i : ι), y i) ↔ ∀ (i : ι), Filter.Tendsto f x (y i)

theorem Filter.tendsto_iInf' {α : 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

theorem Filter.tendsto_iInf_iInf {α : Type u} {β : Type v} {ι : Sort x} {f : α → β} {x : ι → Filter α} {y : ι → Filter β} (h : ∀ (i : ι), Filter.Tendsto f (x i) (y i)) : Filter.Tendsto f (iInf x) (iInf y)

@[simp]

theorem Filter.tendsto_sup {α : Type u} {β : Type v} {f : α → β} {x₁ : Filter α} {x₂ : Filter α} {y : Filter β} : Filter.Tendsto f (x₁ ⊔ x₂) y ↔ Filter.Tendsto f x₁ y ∧ Filter.Tendsto f x₂ y

theorem Filter.Tendsto.sup {α : Type u} {β : Type v} {f : α → β} {x₁ : Filter α} {x₂ : Filter α} {y : Filter β} : Filter.Tendsto f x₁ y → Filter.Tendsto f x₂ y → Filter.Tendsto f (x₁ ⊔ x₂) y

theorem Filter.Tendsto.sup_sup {α : Type u} {β : Type v} {f : α → β} {x₁ : Filter α} {x₂ : Filter α} {y₁ : Filter β} {y₂ : Filter β} (h₁ : Filter.Tendsto f x₁ y₁) (h₂ : Filter.Tendsto f x₂ y₂) : Filter.Tendsto f (x₁ ⊔ x₂) (y₁ ⊔ y₂)

@[simp]

theorem Filter.tendsto_iSup {α : 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

theorem Filter.tendsto_iSup_iSup {α : Type u} {β : Type v} {ι : Sort x} {f : α → β} {x : ι → Filter α} {y : ι → Filter β} (h : ∀ (i : ι), Filter.Tendsto f (x i) (y i)) : Filter.Tendsto f (iSup x) (iSup y)

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

theorem Filter.tendsto_principal_principal {α : Type u} {β : Type v} {f : α → β} {s : Set α} {t : Set β} : Filter.Tendsto f (Filter.principal s) (Filter.principal t) ↔ ∀ a ∈ s, f a ∈ t

@[simp]

theorem Filter.tendsto_pure {α : Type u} {β : Type v} {f : α → β} {a : Filter α} {b : β} : Filter.Tendsto f a (pure b) ↔ ∀ᶠ (x : α) in a, f x = b

theorem Filter.tendsto_pure_pure {α : Type u} {β : Type v} (f : α → β) (a : α) : Filter.Tendsto f (pure a) (pure (f a))

theorem Filter.tendsto_const_pure {α : Type u} {β : Type v} {a : Filter α} {b : β} : Filter.Tendsto (fun (x : α) => b) a (pure b)

theorem Filter.pure_le_iff {α : Type u} {a : α} {l : Filter α} : pure a ≤ l ↔ ∀ s ∈ l, a ∈ s

theorem Filter.tendsto_pure_left {α : Type u} {β : Type v} {f : α → β} {a : α} {l : Filter β} : Filter.Tendsto f (pure a) l ↔ ∀ s ∈ l, f a ∈ s

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

theorem Filter.Tendsto.not_tendsto {α : Type u} {β : Type v} {f : α → β} {a : Filter α} {b₁ : Filter β} {b₂ : Filter β} (hf : Filter.Tendsto f a b₁) [a.NeBot] (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.

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 (fun (x : α) => if p x then f x else g x) l₁ l₂

theorem Filter.Tendsto.if' {α : Type u_2} {β : Type u_3} {l₁ : Filter α} {l₂ : Filter β} {f : α → β} {g : α → β} {p : α → Prop} [DecidablePred p] (hf : Filter.Tendsto f l₁ l₂) (hg : Filter.Tendsto g l₁ l₂) : Filter.Tendsto (fun (a : α) => if p a then f a else g a) l₁ l₂

theorem Filter.Tendsto.piecewise {α : Type u} {β : Type v} {l₁ : Filter α} {l₂ : Filter β} {f : α → β} {g : α → β} {s : Set α} [(x : α) → Decidable (x ∈ s)] (h₀ : Filter.Tendsto f (l₁ ⊓ Filter.principal s) l₂) (h₁ : Filter.Tendsto g (l₁ ⊓ Filter.principal sᶜ) l₂) : Filter.Tendsto (s.piecewise f g) l₁ l₂

theorem Set.EqOn.eventuallyEq {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {g : α → β} (h : Set.EqOn f g s) : f =ᶠ[Filter.principal s] g

theorem Set.EqOn.eventuallyEq_of_mem {α : Type u_1} {β : Type u_2} {s : Set α} {l : Filter α} {f : α → β} {g : α → β} (h : Set.EqOn f g s) (hl : s ∈ l) : f =ᶠ[l] g

theorem HasSubset.Subset.eventuallyLE {α : Type u_1} {l : Filter α} {s : Set α} {t : Set α} (h : s ⊆ t) : s ≤ᶠ[l] t

theorem Set.MapsTo.tendsto {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : Set.MapsTo f s t) : Filter.Tendsto f (Filter.principal s) (Filter.principal t)

theorem Filter.EventuallyEq.comp_tendsto {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} {γ : Type u_3} {f' : α → β} (H : f =ᶠ[l] f') {g : γ → α} {lc : Filter γ} (hg : Filter.Tendsto g lc l) : f ∘ g =ᶠ[lc] f' ∘ g

theorem Filter.map_mapsTo_Iic_iff_tendsto {α : Type u_1} {β : Type u_2} {F : Filter α} {G : Filter β} {m : α → β} : Set.MapsTo (Filter.map m) (Set.Iic F) (Set.Iic G) ↔ Filter.Tendsto m F G

theorem Filter.Tendsto.map_mapsTo_Iic {α : Type u_1} {β : Type u_2} {F : Filter α} {G : Filter β} {m : α → β} : Filter.Tendsto m F G → Set.MapsTo (Filter.map m) (Set.Iic F) (Set.Iic G)

Alias of the reverse direction of Filter.map_mapsTo_Iic_iff_tendsto.

theorem Filter.map_mapsTo_Iic_iff_mapsTo {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {m : α → β} : Set.MapsTo (Filter.map m) (Set.Iic (Filter.principal s)) (Set.Iic (Filter.principal t)) ↔ Set.MapsTo m s t

theorem Set.MapsTo.filter_map_Iic {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {m : α → β} : Set.MapsTo m s t → Set.MapsTo (Filter.map m) (Set.Iic (Filter.principal s)) (Set.Iic (Filter.principal t))

Alias of the reverse direction of Filter.map_mapsTo_Iic_iff_mapsTo.

theorem Filter.map_surjOn_Iic_iff_le_map {α : Type u_1} {β : Type u_2} {F : Filter α} {G : Filter β} {m : α → β} : Set.SurjOn (Filter.map m) (Set.Iic F) (Set.Iic G) ↔ G ≤ Filter.map m F

theorem Filter.map_surjOn_Iic_iff_surjOn {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {m : α → β} : Set.SurjOn (Filter.map m) (Set.Iic (Filter.principal s)) (Set.Iic (Filter.principal t)) ↔ Set.SurjOn m s t

theorem Set.SurjOn.filter_map_Iic {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {m : α → β} : Set.SurjOn m s t → Set.SurjOn (Filter.map m) (Set.Iic (Filter.principal s)) (Set.Iic (Filter.principal t))

Alias of the reverse direction of Filter.map_surjOn_Iic_iff_surjOn.

theorem Filter.filter_injOn_Iic_iff_injOn {α : Type u_1} {β : Type u_2} {s : Set α} {m : α → β} : Set.InjOn (Filter.map m) (Set.Iic (Filter.principal s)) ↔ Set.InjOn m s

theorem Set.InjOn.filter_map_Iic {α : Type u_1} {β : Type u_2} {s : Set α} {m : α → β} : Set.InjOn m s → Set.InjOn (Filter.map m) (Set.Iic (Filter.principal s))

Alias of the reverse direction of Filter.filter_injOn_Iic_iff_injOn.

def Filter.comk {α : Type u_1} (p : Set α → Prop) (he : p ∅) (hmono : ∀ (t : Set α), p t → ∀ s ⊆ t, p s) (hunion : ∀ (s : Set α), p s → ∀ (t : Set α), p t → p (s ∪ t)) : Filter α

Construct a filter from a property that is stable under finite unions. A set s belongs to Filter.comk p _ _ _ iff its complement satisfies the predicate p. This constructor is useful to define filters like Filter.cofinite.

Equations

• Filter.comk p he hmono hunion = { sets := {t : Set α | p tᶜ}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

@[simp]

theorem Filter.mem_comk {α : Type u_1} {p : Set α → Prop} {he : p ∅} {hmono : ∀ (t : Set α), p t → ∀ s ⊆ t, p s} {hunion : ∀ (s : Set α), p s → ∀ (t : Set α), p t → p (s ∪ t)} {s : Set α} : s ∈ Filter.comk p he hmono hunion ↔ p sᶜ

theorem Filter.compl_mem_comk {α : Type u_1} {p : Set α → Prop} {he : p ∅} {hmono : ∀ (t : Set α), p t → ∀ s ⊆ t, p s} {hunion : ∀ (s : Set α), p s → ∀ (t : Set α), p t → p (s ∪ t)} {s : Set α} : sᶜ ∈ Filter.comk p he hmono hunion ↔ p s