Theory of filters on sets

A filter on a type α is a collection of sets of α which contains the whole α, is upwards-closed, and is stable under intersection. 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...

Main definitions

In this file, we endow Filter α 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 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).

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

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.

def Filter.inhabitedMem {α : Type u} {f : Filter α} : Inhabited (Subtype fun (s : Set α) => Membership.mem f s)

Equations

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

theorem Filter.filter_eq_iff {α : Type u} {f g : Filter α} : Iff (Eq f g) (Eq f.sets g.sets)

theorem Filter.sets_subset_sets {α : Type u} {f g : Filter α} : Iff (HasSubset.Subset f.sets g.sets) (LE.le g f)

theorem Filter.sets_ssubset_sets {α : Type u} {f g : Filter α} : Iff (HasSSubset.SSubset f.sets g.sets) (LT.lt g f)

theorem Filter.coext {α : Type u} {f g : Filter α} (h : ∀ (s : Set α), Iff (Membership.mem f (HasCompl.compl s)) (Membership.mem g (HasCompl.compl s))) : Eq 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).

def Filter.instTransSetSupersetMem {α : Type u} : Trans (fun (x1 x2 : Set α) => Superset x1 x2) (fun (x1 : Set α) (x2 : Filter α) => Membership.mem x2 x1) fun (x1 : Set α) (x2 : Filter α) => Membership.mem x2 x1

Equations

• Eq Filter.instTransSetSupersetMem { trans := ⋯ }

def Filter.instTransSetMemSubset {α : Type u} : Trans Membership.mem (fun (x1 x2 : Set α) => HasSubset.Subset x1 x2) Membership.mem

Equations

• Eq Filter.instTransSetMemSubset { trans := ⋯ }

theorem Filter.inter_mem_iff {α : Type u} {f : Filter α} {s t : Set α} : Iff (Membership.mem f (Inter.inter s t)) (And (Membership.mem f s) (Membership.mem f t))

theorem Filter.diff_mem {α : Type u} {f : Filter α} {s t : Set α} (hs : Membership.mem f s) (ht : Membership.mem f (HasCompl.compl t)) : Membership.mem f (SDiff.sdiff s t)

theorem Filter.congr_sets {α : Type u} {f : Filter α} {s t : Set α} (h : Membership.mem f (setOf fun (x : α) => Iff (Membership.mem s x) (Membership.mem t x))) : Iff (Membership.mem f s) (Membership.mem f t)

theorem Filter.copy_eq {α : Type u} {f : Filter α} {S : Set (Set α)} (hmem : ∀ (s : Set α), Iff (Membership.mem S s) (Membership.mem f s)) : Eq (f.copy S hmem) f

theorem Filter.biInter_mem' {α : Type u} {f : Filter α} {β : Type v} {s : β → Set α} {is : Set β} (hf : is.Subsingleton) : Iff (Membership.mem f (Set.iInter fun (i : β) => Set.iInter fun (h : Membership.mem is i) => s i)) (∀ (i : β), Membership.mem is i → Membership.mem f (s i))

Weaker version of Filter.biInter_mem that assumes Subsingleton β rather than Finite β.

theorem Filter.iInter_mem' {α : Type u} {f : Filter α} {β : Sort v} {s : β → Set α} [Subsingleton β] : Iff (Membership.mem f (Set.iInter fun (i : β) => s i)) (∀ (i : β), Membership.mem f (s i))

Weaker version of Filter.iInter_mem that assumes Subsingleton β rather than Finite β.

theorem Filter.exists_mem_subset_iff {α : Type u} {f : Filter α} {s : Set α} : Iff (Exists fun (t : Set α) => And (Membership.mem f t) (HasSubset.Subset t s)) (Membership.mem f s)

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

theorem Filter.exists_mem_and_iff {α : Type u} {f : Filter α} {P Q : Set α → Prop} (hP : Antitone P) (hQ : Antitone Q) : Iff (And (Exists fun (u : Set α) => And (Membership.mem f u) (P u)) (Exists fun (u : Set α) => And (Membership.mem f u) (Q u))) (Exists fun (u : Set α) => And (Membership.mem f u) (And (P u) (Q u)))

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

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

theorem Filter.not_le {α : Type u} {f g : Filter α} : Iff (Not (LE.le f g)) (Exists fun (s : Set α) => And (Membership.mem g s) (Not (Membership.mem f s)))

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 α} : Membership.mem g s → GenerateSets g s
• univ {α : Type u} {g : Set (Set α)} : GenerateSets g Set.univ
• superset {α : Type u} {g : Set (Set α)} {s t : Set α} : GenerateSets g s → HasSubset.Subset s t → GenerateSets g t
• inter {α : Type u} {g : Set (Set α)} {s t : Set α} : GenerateSets g s → GenerateSets g t → GenerateSets g (Inter.inter s t)

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

generate g is the largest filter containing the sets g.

Equations

• Eq (Filter.generate g) { sets := setOf fun (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 : Membership.mem s U) : Membership.mem (generate s) U

theorem Filter.le_generate_iff {α : Type u} {s : Set (Set α)} {f : Filter α} : Iff (LE.le f (generate s)) (HasSubset.Subset s f.sets)

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

def Filter.mkOfClosure {α : Type u} (s : Set (Set α)) (hs : Eq (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

• Eq (Filter.mkOfClosure s hs) { sets := s, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

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

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

Galois insertion from sets of sets into filters.

Equations

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

theorem Filter.mem_inf_iff {α : Type u} {f g : Filter α} {s : Set α} : Iff (Membership.mem (Min.min f g) s) (Exists fun (t₁ : Set α) => And (Membership.mem f t₁) (Exists fun (t₂ : Set α) => And (Membership.mem g t₂) (Eq s (Inter.inter t₁ t₂))))

theorem Filter.mem_inf_of_left {α : Type u} {f g : Filter α} {s : Set α} (h : Membership.mem f s) : Membership.mem (Min.min f g) s

theorem Filter.mem_inf_of_right {α : Type u} {f g : Filter α} {s : Set α} (h : Membership.mem g s) : Membership.mem (Min.min f g) s

theorem Filter.inter_mem_inf {α : Type u} {f g : Filter α} {s t : Set α} (hs : Membership.mem f s) (ht : Membership.mem g t) : Membership.mem (Min.min f g) (Inter.inter s t)

theorem Filter.mem_inf_of_inter {α : Type u} {f g : Filter α} {s t u : Set α} (hs : Membership.mem f s) (ht : Membership.mem g t) (h : HasSubset.Subset (Inter.inter s t) u) : Membership.mem (Min.min f g) u

theorem Filter.mem_inf_iff_superset {α : Type u} {f g : Filter α} {s : Set α} : Iff (Membership.mem (Min.min f g) s) (Exists fun (t₁ : Set α) => And (Membership.mem f t₁) (Exists fun (t₂ : Set α) => And (Membership.mem g t₂) (HasSubset.Subset (Inter.inter t₁ t₂) s)))

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

Complete lattice structure on Filter α.

Equations

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

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

Equations

• Eq Filter.instInhabited { default := Bot.bot }

theorem Filter.NeBot.ne {α : Type u} {f : Filter α} (hf : f.NeBot) : Ne f Bot.bot

theorem Filter.not_neBot {α : Type u} {f : Filter α} : Iff (Not f.NeBot) (Eq f Bot.bot)

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

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

theorem Filter.sup_neBot {α : Type u} {f g : Filter α} : Iff (Max.max f g).NeBot (Or f.NeBot g.NeBot)

theorem Filter.not_disjoint_self_iff {α : Type u} {f : Filter α} : Iff (Not (Disjoint f f)) f.NeBot

theorem Filter.bot_sets_eq {α : Type u} : Eq Bot.bot.sets Set.univ

theorem Filter.eq_or_neBot {α : Type u} (f : Filter α) : Or (Eq f Bot.bot) 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 g : Filter α} : Eq (Max.max f g).sets (Inter.inter f.sets g.sets)

theorem Filter.sSup_sets_eq {α : Type u} {s : Set (Filter α)} : Eq (SupSet.sSup s).sets (Set.iInter fun (f : Filter α) => Set.iInter fun (h : Membership.mem s f) => f.sets)

theorem Filter.iSup_sets_eq {α : Type u} {ι : Sort x} {f : ι → Filter α} : Eq (iSup f).sets (Set.iInter fun (i : ι) => (f i).sets)

theorem Filter.generate_empty {α : Type u} : Eq (generate EmptyCollection.emptyCollection) Top.top

theorem Filter.generate_univ {α : Type u} : Eq (generate Set.univ) Bot.bot

theorem Filter.generate_union {α : Type u} {s t : Set (Set α)} : Eq (generate (Union.union s t)) (Min.min (generate s) (generate t))

theorem Filter.generate_iUnion {α : Type u} {ι : Sort x} {s : ι → Set (Set α)} : Eq (generate (Set.iUnion fun (i : ι) => s i)) (iInf fun (i : ι) => generate (s i))

theorem Filter.mem_sup {α : Type u} {f g : Filter α} {s : Set α} : Iff (Membership.mem (Max.max f g) s) (And (Membership.mem f s) (Membership.mem g s))

theorem Filter.union_mem_sup {α : Type u} {f g : Filter α} {s t : Set α} (hs : Membership.mem f s) (ht : Membership.mem g t) : Membership.mem (Max.max f g) (Union.union s t)

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

theorem Filter.iSup_neBot {α : Type u} {ι : Sort x} {f : ι → Filter α} : Iff (iSup fun (i : ι) => f i).NeBot (Exists fun (i : ι) => (f i).NeBot)

theorem Filter.iInf_eq_generate {α : Type u} {ι : Sort x} (s : ι → Filter α) : Eq (iInf s) (generate (Set.iUnion fun (i : ι) => (s i).sets))

theorem Filter.mem_iInf_of_mem {α : Type u} {ι : Sort x} {f : ι → Filter α} (i : ι) {s : Set α} (hs : Membership.mem (f i) s) : Membership.mem (iInf fun (i : ι) => f i) s

theorem Filter.le_principal_iff {α : Type u} {s : Set α} {f : Filter α} : Iff (LE.le f (principal s)) (Membership.mem f s)

theorem Filter.Iic_principal {α : Type u} (s : Set α) : Eq (Set.Iic (principal s)) (setOf fun (l : Filter α) => Membership.mem l s)

theorem Filter.principal_mono {α : Type u} {s t : Set α} : Iff (LE.le (principal s) (principal t)) (HasSubset.Subset s t)

theorem GCongr.filter_principal_mono {α : Type u} {s t : Set α} : HasSubset.Subset s t → LE.le (Filter.principal s) (Filter.principal t)

Alias of the reverse direction of Filter.principal_mono.

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

theorem Filter.principal_eq_iff_eq {α : Type u} {s t : Set α} : Iff (Eq (principal s) (principal t)) (Eq s t)

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

theorem Filter.principal_univ {α : Type u} : Eq (principal Set.univ) Top.top

theorem Filter.principal_empty {α : Type u} : Eq (principal EmptyCollection.emptyCollection) Bot.bot

theorem Filter.generate_eq_biInf {α : Type u} (S : Set (Set α)) : Eq (generate S) (iInf fun (s : Set α) => iInf fun (h : Membership.mem S s) => principal s)

Lattice equations

theorem Filter.empty_mem_iff_bot {α : Type u} {f : Filter α} : Iff (Membership.mem f EmptyCollection.emptyCollection) (Eq f Bot.bot)

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

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

theorem Filter.empty_not_mem {α : Type u} (f : Filter α) [f.NeBot] : Not (Membership.mem f EmptyCollection.emptyCollection)

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 : Membership.mem f s) : Not (Membership.mem f (HasCompl.compl s))

theorem Filter.filter_eq_bot_of_isEmpty {α : Type u} [IsEmpty α] (f : Filter α) : Eq f Bot.bot

theorem Filter.disjoint_iff {α : Type u} {f g : Filter α} : Iff (Disjoint f g) (Exists fun (s : Set α) => And (Membership.mem f s) (Exists fun (t : Set α) => And (Membership.mem g t) (Disjoint s t)))

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

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

theorem Filter.inf_eq_bot_iff {α : Type u} {f g : Filter α} : Iff (Eq (Min.min f g) Bot.bot) (Exists fun (U : Set α) => And (Membership.mem f U) (Exists fun (V : Set α) => And (Membership.mem g V) (Eq (Inter.inter U V) EmptyCollection.emptyCollection)))

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

There is exactly one filter on an empty type.

Equations

• Eq Filter.unique { default := Bot.bot, 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] : Eq l Top.top

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 α} : Iff (∀ (s : Set α), Membership.mem f s → s.Nonempty) f.NeBot

theorem Filter.instNeBotTop {α : Type u} [Nonempty α] : Top.top.NeBot

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

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

theorem Filter.eq_sInf_of_mem_iff_exists_mem {α : Type u} {S : Set (Filter α)} {l : Filter α} (h : ∀ {s : Set α}, Iff (Membership.mem l s) (Exists fun (f : Filter α) => And (Membership.mem S f) (Membership.mem f s))) : Eq l (InfSet.sInf S)

theorem Filter.eq_iInf_of_mem_iff_exists_mem {α : Type u} {ι : Sort x} {f : ι → Filter α} {l : Filter α} (h : ∀ {s : Set α}, Iff (Membership.mem l s) (Exists fun (i : ι) => Membership.mem (f i) s)) : Eq 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 α}, Iff (Membership.mem l s) (Exists fun (i : ι) => And (p i) (Membership.mem (f i) s))) : Eq l (iInf fun (i : ι) => iInf fun (x : p i) => f i)

theorem Filter.iInf_sets_eq {α : Type u} {ι : Sort x} {f : ι → Filter α} (h : Directed (fun (x1 x2 : Filter α) => GE.ge x1 x2) f) [ne : Nonempty ι] : Eq (iInf f).sets (Set.iUnion fun (i : ι) => (f i).sets)

theorem Filter.mem_iInf_of_directed {α : Type u} {ι : Sort x} {f : ι → Filter α} (h : Directed (fun (x1 x2 : Filter α) => GE.ge x1 x2) f) [Nonempty ι] (s : Set α) : Iff (Membership.mem (iInf f) s) (Exists fun (i : ι) => Membership.mem (f i) s)

theorem Filter.mem_biInf_of_directed {α : Type u} {β : Type v} {f : β → Filter α} {s : Set β} (h : DirectedOn (Order.Preimage f fun (x1 x2 : Filter α) => GE.ge x1 x2) s) (ne : s.Nonempty) {t : Set α} : Iff (Membership.mem (iInf fun (i : β) => iInf fun (h : Membership.mem s i) => f i) t) (Exists fun (i : β) => And (Membership.mem s i) (Membership.mem (f i) t))

theorem Filter.biInf_sets_eq {α : Type u} {β : Type v} {f : β → Filter α} {s : Set β} (h : DirectedOn (Order.Preimage f fun (x1 x2 : Filter α) => GE.ge x1 x2) s) (ne : s.Nonempty) : Eq (iInf fun (i : β) => iInf fun (h : Membership.mem s i) => f i).sets (Set.iUnion fun (i : β) => Set.iUnion fun (h : Membership.mem s i) => (f i).sets)

theorem Filter.sup_join {α : Type u} {f₁ f₂ : Filter (Filter α)} : Eq (Max.max f₁.join f₂.join) (Max.max f₁ f₂).join

theorem Filter.iSup_join {α : Type u} {ι : Sort w} {f : ι → Filter (Filter α)} : Eq (iSup fun (x : ι) => (f x).join) (iSup fun (x : ι) => f x).join

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

Equations

• Eq Filter.instDistribLattice { toLattice := CompleteLattice.toLattice, le_sup_inf := ⋯ }

theorem Filter.iInf_neBot_of_directed' {α : Type u} {ι : Sort x} {f : ι → Filter α} [Nonempty ι] (hd : Directed (fun (x1 x2 : Filter α) => GE.ge x1 x2) 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 (x1 x2 : Filter α) => GE.ge x1 x2) 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 (x1 x2 : Filter α) => GE.ge x1 x2) s) (hbot : Not (Membership.mem s Bot.bot)) : (InfSet.sInf s).NeBot

theorem Filter.sInf_neBot_of_directed {α : Type u} [Nonempty α] {s : Set (Filter α)} (hd : DirectedOn (fun (x1 x2 : Filter α) => GE.ge x1 x2) s) (hbot : Not (Membership.mem s Bot.bot)) : (InfSet.sInf s).NeBot

theorem Filter.iInf_neBot_iff_of_directed' {α : Type u} {ι : Sort x} {f : ι → Filter α} [Nonempty ι] (hd : Directed (fun (x1 x2 : Filter α) => GE.ge x1 x2) f) : Iff (iInf f).NeBot (∀ (i : ι), (f i).NeBot)

theorem Filter.iInf_neBot_iff_of_directed {α : Type u} {ι : Sort x} {f : ι → Filter α} [Nonempty α] (hd : Directed (fun (x1 x2 : Filter α) => GE.ge x1 x2) f) : Iff (iInf f).NeBot (∀ (i : ι), (f i).NeBot)

principal equations

theorem Filter.inf_principal {α : Type u} {s t : Set α} : Eq (Min.min (principal s) (principal t)) (principal (Inter.inter s t))

theorem Filter.sup_principal {α : Type u} {s t : Set α} : Eq (Max.max (principal s) (principal t)) (principal (Union.union s t))

theorem Filter.iSup_principal {α : Type u} {ι : Sort w} {s : ι → Set α} : Eq (iSup fun (x : ι) => principal (s x)) (principal (Set.iUnion fun (i : ι) => s i))

theorem Filter.principal_eq_bot_iff {α : Type u} {s : Set α} : Iff (Eq (principal s) Bot.bot) (Eq s EmptyCollection.emptyCollection)

theorem Filter.principal_neBot_iff {α : Type u} {s : Set α} : Iff (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 (principal s) (principal (HasCompl.compl s))

theorem Filter.mem_inf_principal' {α : Type u} {f : Filter α} {s t : Set α} : Iff (Membership.mem (Min.min f (principal t)) s) (Membership.mem f (Union.union (HasCompl.compl t) s))

theorem Filter.mem_inf_principal {α : Type u} {f : Filter α} {s t : Set α} : Iff (Membership.mem (Min.min f (principal t)) s) (Membership.mem f (setOf fun (x : α) => Membership.mem t x → Membership.mem s x))

theorem Filter.iSup_inf_principal {α : Type u} {ι : Sort x} (f : ι → Filter α) (s : Set α) : Eq (iSup fun (i : ι) => Min.min (f i) (principal s)) (Min.min (iSup fun (i : ι) => f i) (principal s))

theorem Filter.inf_principal_eq_bot {α : Type u} {f : Filter α} {s : Set α} : Iff (Eq (Min.min f (principal s)) Bot.bot) (Membership.mem f (HasCompl.compl s))

theorem Filter.mem_of_eq_bot {α : Type u} {f : Filter α} {s : Set α} (h : Eq (Min.min f (principal (HasCompl.compl s))) Bot.bot) : Membership.mem f s

theorem Filter.diff_mem_inf_principal_compl {α : Type u} {f : Filter α} {s : Set α} (hs : Membership.mem f s) (t : Set α) : Membership.mem (Min.min f (principal (HasCompl.compl t))) (SDiff.sdiff s t)

theorem Filter.principal_le_iff {α : Type u} {s : Set α} {f : Filter α} : Iff (LE.le (principal s) f) (∀ (V : Set α), Membership.mem f V → HasSubset.Subset s V)

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

Eventually

theorem Filter.eventually_iff {α : Type u} {f : Filter α} {P : α → Prop} : Iff (Filter.Eventually (fun (x : α) => P x) f) (Membership.mem f (setOf fun (x : α) => P x))

theorem Filter.eventually_mem_set {α : Type u} {s : Set α} {l : Filter α} : Iff (Filter.Eventually (fun (x : α) => Membership.mem s x) l) (Membership.mem l s)

theorem Filter.ext' {α : Type u} {f₁ f₂ : Filter α} (h : ∀ (p : α → Prop), Iff (Filter.Eventually (fun (x : α) => p x) f₁) (Filter.Eventually (fun (x : α) => p x) f₂)) : Eq f₁ f₂

theorem Filter.Eventually.filter_mono {α : Type u} {f₁ f₂ : Filter α} (h : LE.le f₁ f₂) {p : α → Prop} (hp : Filter.Eventually (fun (x : α) => p x) f₂) : Filter.Eventually (fun (x : α) => p x) f₁

theorem Filter.eventually_of_mem {α : Type u} {f : Filter α} {P : α → Prop} {U : Set α} (hU : Membership.mem f U) (h : ∀ (x : α), Membership.mem U x → P x) : Filter.Eventually (fun (x : α) => P x) f

theorem Filter.Eventually.and {α : Type u} {p q : α → Prop} {f : Filter α} : Filter.Eventually p f → Filter.Eventually q f → Filter.Eventually (fun (x : α) => And (p x) (q x)) f

theorem Filter.eventually_true {α : Type u} (f : Filter α) : Filter.Eventually (fun (x : α) => True) f

theorem Filter.Eventually.of_forall {α : Type u} {p : α → Prop} {f : Filter α} (hp : ∀ (x : α), p x) : Filter.Eventually (fun (x : α) => p x) f

theorem Filter.eventually_false_iff_eq_bot {α : Type u} {f : Filter α} : Iff (Filter.Eventually (fun (x : α) => False) f) (Eq f Bot.bot)

theorem Filter.eventually_const {α : Type u} {f : Filter α} [t : f.NeBot] {p : Prop} : Iff (Filter.Eventually (fun (x : α) => p) f) p

theorem Filter.eventually_iff_exists_mem {α : Type u} {p : α → Prop} {f : Filter α} : Iff (Filter.Eventually (fun (x : α) => p x) f) (Exists fun (v : Set α) => And (Membership.mem f v) (∀ (y : α), Membership.mem v y → p y))

theorem Filter.Eventually.exists_mem {α : Type u} {p : α → Prop} {f : Filter α} (hp : Filter.Eventually (fun (x : α) => p x) f) : Exists fun (v : Set α) => And (Membership.mem f v) (∀ (y : α), Membership.mem v y → p y)

theorem Filter.Eventually.mp {α : Type u} {p q : α → Prop} {f : Filter α} (hp : Filter.Eventually (fun (x : α) => p x) f) (hq : Filter.Eventually (fun (x : α) => p x → q x) f) : Filter.Eventually (fun (x : α) => q x) f

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

theorem Filter.forall_eventually_of_eventually_forall {α : Type u} {β : Type v} {f : Filter α} {p : α → β → Prop} (h : Filter.Eventually (fun (x : α) => ∀ (y : β), p x y) f) (y : β) : Filter.Eventually (fun (x : α) => p x y) f

theorem Filter.eventually_and {α : Type u} {p q : α → Prop} {f : Filter α} : Iff (Filter.Eventually (fun (x : α) => And (p x) (q x)) f) (And (Filter.Eventually (fun (x : α) => p x) f) (Filter.Eventually (fun (x : α) => q x) f))

theorem Filter.Eventually.congr {α : Type u} {f : Filter α} {p q : α → Prop} (h' : Filter.Eventually (fun (x : α) => p x) f) (h : Filter.Eventually (fun (x : α) => Iff (p x) (q x)) f) : Filter.Eventually (fun (x : α) => q x) f

theorem Filter.eventually_congr {α : Type u} {f : Filter α} {p q : α → Prop} (h : Filter.Eventually (fun (x : α) => Iff (p x) (q x)) f) : Iff (Filter.Eventually (fun (x : α) => p x) f) (Filter.Eventually (fun (x : α) => q x) f)

theorem Filter.eventually_or_distrib_left {α : Type u} {f : Filter α} {p : Prop} {q : α → Prop} : Iff (Filter.Eventually (fun (x : α) => Or p (q x)) f) (Or p (Filter.Eventually (fun (x : α) => q x) f))

theorem Filter.eventually_or_distrib_right {α : Type u} {f : Filter α} {p : α → Prop} {q : Prop} : Iff (Filter.Eventually (fun (x : α) => Or (p x) q) f) (Or (Filter.Eventually (fun (x : α) => p x) f) q)

theorem Filter.eventually_imp_distrib_left {α : Type u} {f : Filter α} {p : Prop} {q : α → Prop} : Iff (Filter.Eventually (fun (x : α) => p → q x) f) (p → Filter.Eventually (fun (x : α) => q x) f)

theorem Filter.eventually_bot {α : Type u} {p : α → Prop} : Filter.Eventually (fun (x : α) => p x) Bot.bot

theorem Filter.eventually_top {α : Type u} {p : α → Prop} : Iff (Filter.Eventually (fun (x : α) => p x) Top.top) (∀ (x : α), p x)

theorem Filter.eventually_sup {α : Type u} {p : α → Prop} {f g : Filter α} : Iff (Filter.Eventually (fun (x : α) => p x) (Max.max f g)) (And (Filter.Eventually (fun (x : α) => p x) f) (Filter.Eventually (fun (x : α) => p x) g))

theorem Filter.eventually_sSup {α : Type u} {p : α → Prop} {fs : Set (Filter α)} : Iff (Filter.Eventually (fun (x : α) => p x) (SupSet.sSup fs)) (∀ (f : Filter α), Membership.mem fs f → Filter.Eventually (fun (x : α) => p x) f)

theorem Filter.eventually_iSup {α : Type u} {ι : Sort x} {p : α → Prop} {fs : ι → Filter α} : Iff (Filter.Eventually (fun (x : α) => p x) (iSup fun (b : ι) => fs b)) (∀ (b : ι), Filter.Eventually (fun (x : α) => p x) (fs b))

theorem Filter.eventually_principal {α : Type u} {a : Set α} {p : α → Prop} : Iff (Filter.Eventually (fun (x : α) => p x) (principal a)) (∀ (x : α), Membership.mem a x → p x)

theorem Filter.Eventually.forall_mem {α : Type u_2} {f : Filter α} {s : Set α} {P : α → Prop} (hP : Filter.Eventually (fun (x : α) => P x) f) (hf : LE.le (principal s) f) (x : α) : Membership.mem s x → P x

theorem Filter.eventually_inf {α : Type u} {f g : Filter α} {p : α → Prop} : Iff (Filter.Eventually (fun (x : α) => p x) (Min.min f g)) (Exists fun (s : Set α) => And (Membership.mem f s) (Exists fun (t : Set α) => And (Membership.mem g t) (∀ (x : α), Membership.mem (Inter.inter s t) x → p x)))

theorem Filter.eventually_inf_principal {α : Type u} {f : Filter α} {p : α → Prop} {s : Set α} : Iff (Filter.Eventually (fun (x : α) => p x) (Min.min f (principal s))) (Filter.Eventually (fun (x : α) => Membership.mem s x → p x) f)

theorem Filter.eventually_iff_all_subsets {α : Type u} {f : Filter α} {p : α → Prop} : Iff (Filter.Eventually (fun (x : α) => p x) f) (∀ (s : Set α), Filter.Eventually (fun (x : α) => Membership.mem s x → p x) f)

Frequently

theorem Filter.Eventually.frequently {α : Type u} {f : Filter α} [f.NeBot] {p : α → Prop} (h : Filter.Eventually (fun (x : α) => p x) f) : Filter.Frequently (fun (x : α) => p x) f

theorem Filter.Frequently.of_forall {α : Type u} {f : Filter α} [f.NeBot] {p : α → Prop} (h : ∀ (x : α), p x) : Filter.Frequently (fun (x : α) => p x) f

theorem Filter.Frequently.mp {α : Type u} {p q : α → Prop} {f : Filter α} (h : Filter.Frequently (fun (x : α) => p x) f) (hpq : Filter.Eventually (fun (x : α) => p x → q x) f) : Filter.Frequently (fun (x : α) => q x) f

theorem Filter.frequently_congr {α : Type u} {p q : α → Prop} {f : Filter α} (h : Filter.Eventually (fun (x : α) => Iff (p x) (q x)) f) : Iff (Filter.Frequently (fun (x : α) => p x) f) (Filter.Frequently (fun (x : α) => q x) f)

theorem Filter.Frequently.filter_mono {α : Type u} {p : α → Prop} {f g : Filter α} (h : Filter.Frequently (fun (x : α) => p x) f) (hle : LE.le f g) : Filter.Frequently (fun (x : α) => p x) g

theorem Filter.Frequently.mono {α : Type u} {p q : α → Prop} {f : Filter α} (h : Filter.Frequently (fun (x : α) => p x) f) (hpq : ∀ (x : α), p x → q x) : Filter.Frequently (fun (x : α) => q x) f

theorem Filter.Frequently.and_eventually {α : Type u} {p q : α → Prop} {f : Filter α} (hp : Filter.Frequently (fun (x : α) => p x) f) (hq : Filter.Eventually (fun (x : α) => q x) f) : Filter.Frequently (fun (x : α) => And (p x) (q x)) f

theorem Filter.Eventually.and_frequently {α : Type u} {p q : α → Prop} {f : Filter α} (hp : Filter.Eventually (fun (x : α) => p x) f) (hq : Filter.Frequently (fun (x : α) => q x) f) : Filter.Frequently (fun (x : α) => And (p x) (q x)) f

theorem Filter.Frequently.exists {α : Type u} {p : α → Prop} {f : Filter α} (hp : Filter.Frequently (fun (x : α) => p x) f) : Exists fun (x : α) => p x

theorem Filter.Eventually.exists {α : Type u} {p : α → Prop} {f : Filter α} [f.NeBot] (hp : Filter.Eventually (fun (x : α) => p x) f) : Exists fun (x : α) => p x

theorem Filter.frequently_iff_neBot {α : Type u} {l : Filter α} {p : α → Prop} : Iff (Filter.Frequently (fun (x : α) => p x) l) (Min.min l (principal (setOf fun (x : α) => p x))).NeBot

theorem Filter.frequently_mem_iff_neBot {α : Type u} {l : Filter α} {s : Set α} : Iff (Filter.Frequently (fun (x : α) => Membership.mem s x) l) (Min.min l (principal s)).NeBot

theorem Filter.frequently_iff_forall_eventually_exists_and {α : Type u} {p : α → Prop} {f : Filter α} : Iff (Filter.Frequently (fun (x : α) => p x) f) (∀ {q : α → Prop}, Filter.Eventually (fun (x : α) => q x) f → Exists fun (x : α) => And (p x) (q x))

theorem Filter.frequently_iff {α : Type u} {f : Filter α} {P : α → Prop} : Iff (Filter.Frequently (fun (x : α) => P x) f) (∀ {U : Set α}, Membership.mem f U → Exists fun (x : α) => And (Membership.mem U x) (P x))

theorem Filter.not_eventually {α : Type u} {p : α → Prop} {f : Filter α} : Iff (Not (Filter.Eventually (fun (x : α) => p x) f)) (Filter.Frequently (fun (x : α) => Not (p x)) f)

theorem Filter.not_frequently {α : Type u} {p : α → Prop} {f : Filter α} : Iff (Not (Filter.Frequently (fun (x : α) => p x) f)) (Filter.Eventually (fun (x : α) => Not (p x)) f)

theorem Filter.frequently_true_iff_neBot {α : Type u} (f : Filter α) : Iff (Filter.Frequently (fun (x : α) => True) f) f.NeBot

theorem Filter.frequently_false {α : Type u} (f : Filter α) : Not (Filter.Frequently (fun (x : α) => False) f)

theorem Filter.frequently_const {α : Type u} {f : Filter α} [f.NeBot] {p : Prop} : Iff (Filter.Frequently (fun (x : α) => p) f) p

theorem Filter.frequently_or_distrib {α : Type u} {f : Filter α} {p q : α → Prop} : Iff (Filter.Frequently (fun (x : α) => Or (p x) (q x)) f) (Or (Filter.Frequently (fun (x : α) => p x) f) (Filter.Frequently (fun (x : α) => q x) f))

theorem Filter.frequently_or_distrib_left {α : Type u} {f : Filter α} [f.NeBot] {p : Prop} {q : α → Prop} : Iff (Filter.Frequently (fun (x : α) => Or p (q x)) f) (Or p (Filter.Frequently (fun (x : α) => q x) f))

theorem Filter.frequently_or_distrib_right {α : Type u} {f : Filter α} [f.NeBot] {p : α → Prop} {q : Prop} : Iff (Filter.Frequently (fun (x : α) => Or (p x) q) f) (Or (Filter.Frequently (fun (x : α) => p x) f) q)

theorem Filter.frequently_imp_distrib {α : Type u} {f : Filter α} {p q : α → Prop} : Iff (Filter.Frequently (fun (x : α) => p x → q x) f) (Filter.Eventually (fun (x : α) => p x) f → Filter.Frequently (fun (x : α) => q x) f)

theorem Filter.frequently_imp_distrib_left {α : Type u} {f : Filter α} [f.NeBot] {p : Prop} {q : α → Prop} : Iff (Filter.Frequently (fun (x : α) => p → q x) f) (p → Filter.Frequently (fun (x : α) => q x) f)

theorem Filter.frequently_imp_distrib_right {α : Type u} {f : Filter α} [f.NeBot] {p : α → Prop} {q : Prop} : Iff (Filter.Frequently (fun (x : α) => p x → q) f) (Filter.Eventually (fun (x : α) => p x) f → q)

theorem Filter.eventually_imp_distrib_right {α : Type u} {f : Filter α} {p : α → Prop} {q : Prop} : Iff (Filter.Eventually (fun (x : α) => p x → q) f) (Filter.Frequently (fun (x : α) => p x) f → q)

theorem Filter.frequently_and_distrib_left {α : Type u} {f : Filter α} {p : Prop} {q : α → Prop} : Iff (Filter.Frequently (fun (x : α) => And p (q x)) f) (And p (Filter.Frequently (fun (x : α) => q x) f))

theorem Filter.frequently_and_distrib_right {α : Type u} {f : Filter α} {p : α → Prop} {q : Prop} : Iff (Filter.Frequently (fun (x : α) => And (p x) q) f) (And (Filter.Frequently (fun (x : α) => p x) f) q)

theorem Filter.frequently_bot {α : Type u} {p : α → Prop} : Not (Filter.Frequently (fun (x : α) => p x) Bot.bot)

theorem Filter.frequently_top {α : Type u} {p : α → Prop} : Iff (Filter.Frequently (fun (x : α) => p x) Top.top) (Exists fun (x : α) => p x)

theorem Filter.frequently_principal {α : Type u} {a : Set α} {p : α → Prop} : Iff (Filter.Frequently (fun (x : α) => p x) (principal a)) (Exists fun (x : α) => And (Membership.mem a x) (p x))

theorem Filter.frequently_inf_principal {α : Type u} {f : Filter α} {s : Set α} {p : α → Prop} : Iff (Filter.Frequently (fun (x : α) => p x) (Min.min f (principal s))) (Filter.Frequently (fun (x : α) => And (Membership.mem s x) (p x)) f)

theorem Filter.Frequently.of_inf_principal {α : Type u} {f : Filter α} {s : Set α} {p : α → Prop} : Filter.Frequently (fun (x : α) => p x) (Min.min f (principal s)) → Filter.Frequently (fun (x : α) => And (Membership.mem s x) (p x)) f

Alias of the forward direction of Filter.frequently_inf_principal.

theorem Filter.Frequently.inf_principal {α : Type u} {f : Filter α} {s : Set α} {p : α → Prop} : Filter.Frequently (fun (x : α) => And (Membership.mem s x) (p x)) f → Filter.Frequently (fun (x : α) => p x) (Min.min f (principal s))

Alias of the reverse direction of Filter.frequently_inf_principal.

theorem Filter.frequently_sup {α : Type u} {p : α → Prop} {f g : Filter α} : Iff (Filter.Frequently (fun (x : α) => p x) (Max.max f g)) (Or (Filter.Frequently (fun (x : α) => p x) f) (Filter.Frequently (fun (x : α) => p x) g))

theorem Filter.frequently_sSup {α : Type u} {p : α → Prop} {fs : Set (Filter α)} : Iff (Filter.Frequently (fun (x : α) => p x) (SupSet.sSup fs)) (Exists fun (f : Filter α) => And (Membership.mem fs f) (Filter.Frequently (fun (x : α) => p x) f))

theorem Filter.frequently_iSup {α : Type u} {β : Type v} {p : α → Prop} {fs : β → Filter α} : Iff (Filter.Frequently (fun (x : α) => p x) (iSup fun (b : β) => fs b)) (Exists fun (b : β) => Filter.Frequently (fun (x : α) => p x) (fs b))

theorem Filter.Eventually.choice {α : Type u} {β : Type v} {r : α → β → Prop} {l : Filter α} [l.NeBot] (h : Filter.Eventually (fun (x : α) => Exists fun (y : β) => r x y) l) : Exists fun (f : α → β) => Filter.Eventually (fun (x : α) => r x (f x)) l

theorem Filter.skolem {ι : Type u_2} {α : ι → Type u_3} [∀ (i : ι), Nonempty (α i)] {P : (i : ι) → α i → Prop} {F : Filter ι} : Iff (Filter.Eventually (fun (i : ι) => Exists fun (b : α i) => P i b) F) (Exists fun (b : (i : ι) → α i) => Filter.Eventually (fun (i : ι) => P i (b i)) F)

Relation “eventually equal”

theorem Filter.EventuallyEq.eventually {α : Type u} {β : Type v} {l : Filter α} {f g : α → β} (h : l.EventuallyEq f g) : Filter.Eventually (fun (x : α) => Eq (f x) (g x)) l

theorem Filter.eventuallyEq_top {α : Type u} {β : Type v} {f g : α → β} : Iff (Top.top.EventuallyEq f g) (Eq f g)

theorem Filter.EventuallyEq.rw {α : Type u} {β : Type v} {l : Filter α} {f g : α → β} (h : l.EventuallyEq f g) (p : α → β → Prop) (hf : Filter.Eventually (fun (x : α) => p x (f x)) l) : Filter.Eventually (fun (x : α) => p x (g x)) l

theorem Filter.eventuallyEq_set {α : Type u} {s t : Set α} {l : Filter α} : Iff (l.EventuallyEq s t) (Filter.Eventually (fun (x : α) => Iff (Membership.mem s x) (Membership.mem t x)) l)

theorem Filter.EventuallyEq.mem_iff {α : Type u} {s t : Set α} {l : Filter α} : l.EventuallyEq s t → Filter.Eventually (fun (x : α) => Iff (Membership.mem s x) (Membership.mem t x)) l

Alias of the forward direction of Filter.eventuallyEq_set.

theorem Filter.Eventually.set_eq {α : Type u} {s t : Set α} {l : Filter α} : Filter.Eventually (fun (x : α) => Iff (Membership.mem s x) (Membership.mem t x)) l → l.EventuallyEq s t

Alias of the reverse direction of Filter.eventuallyEq_set.

theorem Filter.eventuallyEq_univ {α : Type u} {s : Set α} {l : Filter α} : Iff (l.EventuallyEq s Set.univ) (Membership.mem l s)

theorem Filter.EventuallyEq.exists_mem {α : Type u} {β : Type v} {l : Filter α} {f g : α → β} (h : l.EventuallyEq f g) : Exists fun (s : Set α) => And (Membership.mem l s) (Set.EqOn f g s)

theorem Filter.eventuallyEq_of_mem {α : Type u} {β : Type v} {l : Filter α} {f g : α → β} {s : Set α} (hs : Membership.mem l s) (h : Set.EqOn f g s) : l.EventuallyEq f g

theorem Filter.eventuallyEq_iff_exists_mem {α : Type u} {β : Type v} {l : Filter α} {f g : α → β} : Iff (l.EventuallyEq f g) (Exists fun (s : Set α) => And (Membership.mem l s) (Set.EqOn f g s))

theorem Filter.EventuallyEq.filter_mono {α : Type u} {β : Type v} {l l' : Filter α} {f g : α → β} (h₁ : l.EventuallyEq f g) (h₂ : LE.le l' l) : l'.EventuallyEq f g

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

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

theorem Filter.EventuallyEq.of_eq {α : Type u} {β : Type v} {l : Filter α} {f g : α → β} (h : Eq f g) : l.EventuallyEq f g

theorem Eq.eventuallyEq {α : Type u} {β : Type v} {l : Filter α} {f g : α → β} (h : Eq f g) : l.EventuallyEq f g

Alias of Filter.EventuallyEq.of_eq.

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

theorem Filter.eventuallyEq_comm {α : Type u} {β : Type v} {f g : α → β} {l : Filter α} : Iff (l.EventuallyEq f g) (l.EventuallyEq g f)

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

theorem Filter.EventuallyEq.congr_left {α : Type u} {β : Type v} {l : Filter α} {f g h : α → β} (H : l.EventuallyEq f g) : Iff (l.EventuallyEq f h) (l.EventuallyEq g h)

theorem Filter.EventuallyEq.congr_right {α : Type u} {β : Type v} {l : Filter α} {f g h : α → β} (H : l.EventuallyEq g h) : Iff (l.EventuallyEq f g) (l.EventuallyEq f h)

def Filter.instTransForallEventuallyEq {α : Type u} {β : Type v} {l : Filter α} : Trans (fun (x1 x2 : α → β) => l.EventuallyEq x1 x2) (fun (x1 x2 : α → β) => l.EventuallyEq x1 x2) fun (x1 x2 : α → β) => l.EventuallyEq x1 x2

Equations

• Eq Filter.instTransForallEventuallyEq { trans := ⋯ }

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

@[deprecated Filter.EventuallyEq.prodMk (since := "2025-03-10")]

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

Alias of Filter.EventuallyEq.prodMk.

theorem Filter.EventuallyEq.fun_comp {α : Type u} {β : Type v} {γ : Type w} {f g : α → β} {l : Filter α} (H : l.EventuallyEq f g) (h : β → γ) : l.EventuallyEq (Function.comp h f) (Function.comp h g)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Filter.EventuallyEq.preimage {α : Type u} {β : Type v} {l : Filter α} {f g : α → β} (h : l.EventuallyEq f g) (s : Set β) : l.EventuallyEq (Set.preimage f s) (Set.preimage g s)

theorem Filter.EventuallyEq.inter {α : Type u} {s t s' t' : Set α} {l : Filter α} (h : l.EventuallyEq s t) (h' : l.EventuallyEq s' t') : l.EventuallyEq (Inter.inter s s') (Inter.inter t t')

theorem Filter.EventuallyEq.union {α : Type u} {s t s' t' : Set α} {l : Filter α} (h : l.EventuallyEq s t) (h' : l.EventuallyEq s' t') : l.EventuallyEq (Union.union s s') (Union.union t t')

theorem Filter.EventuallyEq.compl {α : Type u} {s t : Set α} {l : Filter α} (h : l.EventuallyEq s t) : l.EventuallyEq (HasCompl.compl s) (HasCompl.compl t)

theorem Filter.EventuallyEq.diff {α : Type u} {s t s' t' : Set α} {l : Filter α} (h : l.EventuallyEq s t) (h' : l.EventuallyEq s' t') : l.EventuallyEq (SDiff.sdiff s s') (SDiff.sdiff t t')

theorem Filter.EventuallyEq.symmDiff {α : Type u} {s t s' t' : Set α} {l : Filter α} (h : l.EventuallyEq s t) (h' : l.EventuallyEq s' t') : l.EventuallyEq (symmDiff s s') (symmDiff t t')

theorem Filter.eventuallyEq_empty {α : Type u} {s : Set α} {l : Filter α} : Iff (l.EventuallyEq s EmptyCollection.emptyCollection) (Filter.Eventually (fun (x : α) => Not (Membership.mem s x)) l)

theorem Filter.inter_eventuallyEq_left {α : Type u} {s t : Set α} {l : Filter α} : Iff (l.EventuallyEq (Inter.inter s t) s) (Filter.Eventually (fun (x : α) => Membership.mem s x → Membership.mem t x) l)

theorem Filter.inter_eventuallyEq_right {α : Type u} {s t : Set α} {l : Filter α} : Iff (l.EventuallyEq (Inter.inter s t) t) (Filter.Eventually (fun (x : α) => Membership.mem t x → Membership.mem s x) l)

theorem Filter.eventuallyEq_principal {α : Type u} {β : Type v} {s : Set α} {f g : α → β} : Iff ((principal s).EventuallyEq f g) (Set.EqOn f g s)

theorem Filter.eventuallyEq_inf_principal_iff {α : Type u} {β : Type v} {F : Filter α} {s : Set α} {f g : α → β} : Iff ((Min.min F (principal s)).EventuallyEq f g) (Filter.Eventually (fun (x : α) => Membership.mem s x → Eq (f x) (g x)) F)

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

theorem Filter.eventuallyEq_iff_sub {α : Type u} {β : Type v} [AddGroup β] {f g : α → β} {l : Filter α} : Iff (l.EventuallyEq f g) (l.EventuallyEq (HSub.hSub f g) 0)

theorem Filter.eventuallyEq_iff_all_subsets {α : Type u} {β : Type v} {f g : α → β} {l : Filter α} : Iff (l.EventuallyEq f g) (∀ (s : Set α), Filter.Eventually (fun (x : α) => Membership.mem s x → Eq (f x) (g x)) l)

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

theorem Filter.eventuallyLE_congr {α : Type u} {β : Type v} [LE β] {l : Filter α} {f f' g g' : α → β} (hf : l.EventuallyEq f f') (hg : l.EventuallyEq g g') : Iff (l.EventuallyLE f g) (l.EventuallyLE f' g')

theorem Filter.eventuallyLE_iff_all_subsets {α : Type u} {β : Type v} [LE β] {f g : α → β} {l : Filter α} : Iff (l.EventuallyLE f g) (∀ (s : Set α), Filter.Eventually (fun (x : α) => Membership.mem s x → LE.le (f x) (g x)) l)

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

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

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

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

def Filter.instTransForallEventuallyLE {α : Type u} {β : Type v} [Preorder β] {l : Filter α} : Trans (fun (x1 x2 : α → β) => l.EventuallyLE x1 x2) (fun (x1 x2 : α → β) => l.EventuallyLE x1 x2) fun (x1 x2 : α → β) => l.EventuallyLE x1 x2

Equations

• Eq Filter.instTransForallEventuallyLE { trans := ⋯ }

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

def Filter.instTransForallEventuallyEqEventuallyLE {α : Type u} {β : Type v} [Preorder β] {l : Filter α} : Trans (fun (x1 x2 : α → β) => l.EventuallyEq x1 x2) (fun (x1 x2 : α → β) => l.EventuallyLE x1 x2) fun (x1 x2 : α → β) => l.EventuallyLE x1 x2

Equations

• Eq Filter.instTransForallEventuallyEqEventuallyLE { trans := ⋯ }

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

def Filter.instTransForallEventuallyLEEventuallyEq {α : Type u} {β : Type v} [Preorder β] {l : Filter α} : Trans (fun (x1 x2 : α → β) => l.EventuallyLE x1 x2) (fun (x1 x2 : α → β) => l.EventuallyEq x1 x2) fun (x1 x2 : α → β) => l.EventuallyLE x1 x2

Equations

• Eq Filter.instTransForallEventuallyLEEventuallyEq { trans := ⋯ }

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

theorem Filter.eventuallyLE_antisymm_iff {α : Type u} {β : Type v} [PartialOrder β] {l : Filter α} {f g : α → β} : Iff (l.EventuallyEq f g) (And (l.EventuallyLE f g) (l.EventuallyLE g f))

theorem Filter.EventuallyLE.le_iff_eq {α : Type u} {β : Type v} [PartialOrder β] {l : Filter α} {f g : α → β} (h : l.EventuallyLE f g) : Iff (l.EventuallyLE g f) (l.EventuallyEq g f)

theorem Filter.Eventually.ne_of_lt {α : Type u} {β : Type v} [Preorder β] {l : Filter α} {f g : α → β} (h : Filter.Eventually (fun (x : α) => LT.lt (f x) (g x)) l) : Filter.Eventually (fun (x : α) => Ne (f x) (g x)) l

theorem Filter.Eventually.ne_top_of_lt {α : Type u} {β : Type v} [Preorder β] [OrderTop β] {l : Filter α} {f g : α → β} (h : Filter.Eventually (fun (x : α) => LT.lt (f x) (g x)) l) : Filter.Eventually (fun (x : α) => Ne (f x) Top.top) l

theorem Filter.Eventually.lt_top_of_ne {α : Type u} {β : Type v} [PartialOrder β] [OrderTop β] {l : Filter α} {f : α → β} (h : Filter.Eventually (fun (x : α) => Ne (f x) Top.top) l) : Filter.Eventually (fun (x : α) => LT.lt (f x) Top.top) l

theorem Filter.Eventually.lt_top_iff_ne_top {α : Type u} {β : Type v} [PartialOrder β] [OrderTop β] {l : Filter α} {f : α → β} : Iff (Filter.Eventually (fun (x : α) => LT.lt (f x) Top.top) l) (Filter.Eventually (fun (x : α) => Ne (f x) Top.top) l)

theorem Filter.EventuallyLE.inter {α : Type u} {s t s' t' : Set α} {l : Filter α} (h : l.EventuallyLE s t) (h' : l.EventuallyLE s' t') : l.EventuallyLE (Inter.inter s s') (Inter.inter t t')

theorem Filter.EventuallyLE.union {α : Type u} {s t s' t' : Set α} {l : Filter α} (h : l.EventuallyLE s t) (h' : l.EventuallyLE s' t') : l.EventuallyLE (Union.union s s') (Union.union t t')

theorem Filter.EventuallyLE.compl {α : Type u} {s t : Set α} {l : Filter α} (h : l.EventuallyLE s t) : l.EventuallyLE (HasCompl.compl t) (HasCompl.compl s)

theorem Filter.EventuallyLE.diff {α : Type u} {s t s' t' : Set α} {l : Filter α} (h : l.EventuallyLE s t) (h' : l.EventuallyLE t' s') : l.EventuallyLE (SDiff.sdiff s s') (SDiff.sdiff t t')

theorem Filter.set_eventuallyLE_iff_mem_inf_principal {α : Type u} {s t : Set α} {l : Filter α} : Iff (l.EventuallyLE s t) (Membership.mem (Min.min l (principal s)) t)

theorem Filter.set_eventuallyLE_iff_inf_principal_le {α : Type u} {s t : Set α} {l : Filter α} : Iff (l.EventuallyLE s t) (LE.le (Min.min l (principal s)) (Min.min l (principal t)))

theorem Filter.set_eventuallyEq_iff_inf_principal {α : Type u} {s t : Set α} {l : Filter α} : Iff (l.EventuallyEq s t) (Eq (Min.min l (principal s)) (Min.min l (principal t)))

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

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

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

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

theorem Filter.join_le {α : Type u} {f : Filter (Filter α)} {l : Filter α} (h : Filter.Eventually (fun (m : Filter α) => LE.le m l) f) : LE.le f.join l

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

theorem Set.EqOn.eventuallyEq_of_mem {α : Type u_1} {β : Type u_2} {s : Set α} {l : Filter α} {f g : α → β} (h : EqOn f g s) (hl : Membership.mem l s) : l.EventuallyEq f g

theorem HasSubset.Subset.eventuallyLE {α : Type u_1} {l : Filter α} {s t : Set α} (h : Subset s t) : l.EventuallyLE s t

theorem Filter.compl_mem_comk {α : Type u_1} {p : Set α → Prop} {he : p EmptyCollection.emptyCollection} {hmono : ∀ (t : Set α), p t → ∀ (s : Set α), HasSubset.Subset s t → p s} {hunion : ∀ (s : Set α), p s → ∀ (t : Set α), p t → p (Union.union s t)} {s : Set α} : Iff (Membership.mem (comk p he hmono hunion) (HasCompl.compl s)) (p s)