Mathlib.Order.Filter.Basic

Filter.inhabitedMem instance

: Inhabited { s : Set α // s ∈ f }

Full source

instance inhabitedMem : Inhabited { s : Set α // s ∈ f } :=
  ⟨⟨univ, f.univ_sets⟩⟩

Nonempty Filter Membership

Informal description

For any filter $f$ on a type $\alpha$, the collection of sets belonging to $f$ is nonempty.

Filter.filter_eq_iff theorem

: f = g ↔ f.sets = g.sets

Full source

theorem filter_eq_iff : f = g ↔ f.sets = g.sets :=
  ⟨congr_arg _, filter_eq⟩

Filter Equality via Set Equality

Informal description

Two filters $f$ and $g$ on a type $\alpha$ are equal if and only if their collections of sets are equal, i.e., $f = g \leftrightarrow f.\text{sets} = g.\text{sets}$.

Filter.sets_subset_sets theorem

: f.sets ⊆ g.sets ↔ g ≤ f

Full source

@[simp] theorem sets_subset_sets : f.sets ⊆ g.setsf.sets ⊆ g.sets ↔ g ≤ f := .rfl

Filter refinement via set inclusion: $f.\text{sets} \subseteq g.\text{sets} \leftrightarrow g \leq f$

Informal description

For two filters $f$ and $g$ on a type $\alpha$, the collection of sets in $f$ is a subset of the collection of sets in $g$ if and only if $g$ is finer than $f$ (i.e., $g \leq f$ in the partial order of filters).

Filter.sets_ssubset_sets theorem

: f.sets ⊂ g.sets ↔ g < f

Full source

@[simp] theorem sets_ssubset_sets : f.sets ⊂ g.setsf.sets ⊂ g.sets ↔ g < f := .rfl

Strict Filter Refinement via Strict Set Inclusion: $f.\text{sets} \subset g.\text{sets} \leftrightarrow g < f$

Informal description

For two filters $f$ and $g$ on a type $\alpha$, the collection of sets in $f$ is a strict subset of the collection of sets in $g$ if and only if $g$ is strictly finer than $f$ (i.e., $g < f$ in the partial order of filters).

Filter.coext theorem

(h : ∀ s, sᶜ ∈ f ↔ sᶜ ∈ g) : f = g

Full source

/-- An extensionality lemma that is useful for filters with good lemmas about `sᶜ ∈ f` (e.g.,
`Filter.comap`, `Filter.coprod`, `Filter.Coprod`, `Filter.cofinite`). -/
protected theorem coext (h : ∀ s, sᶜsᶜ ∈ fsᶜ ∈ f ↔ sᶜ ∈ g) : f = g :=
  Filter.ext <| compl_surjective.forall.2 h

Filter Extensionality via Complements: $f = g \iff \forall s, s^\complement \in f \leftrightarrow s^\complement \in g$

Informal description

For any two filters $f$ and $g$ on a type $\alpha$, if for every subset $s$ of $\alpha$ the complement $s^\complement$ belongs to $f$ if and only if it belongs to $g$, then $f = g$.

Filter.instTransSetSupersetMem instance

: Trans (· ⊇ ·) ((· ∈ ·) : Set α → Filter α → Prop) (· ∈ ·)

Full source

instance : Trans (· ⊇ ·) ((· ∈ ·) : Set α → Filter α → Prop) (· ∈ ·) where
  trans h₁ h₂ := mem_of_superset h₂ h₁

Transitivity of Superset Relation with Filter Membership

Informal description

For any type $\alpha$, the relation $\supseteq$ on subsets of $\alpha$ is transitive with respect to the membership relation $\in$ in filters on $\alpha$. That is, if $s \supseteq t$ and $t \in f$, then $s \in f$ for any subsets $s, t \subseteq \alpha$ and any filter $f$ on $\alpha$.

Filter.instTransSetMemSubset instance

: Trans Membership.mem (· ⊆ ·) (Membership.mem : Filter α → Set α → Prop)

Full source

instance : Trans Membership.mem (· ⊆ ·) (Membership.mem : Filter α → Set α → Prop) where
  trans h₁ h₂ := mem_of_superset h₁ h₂

Transitivity of Filter Membership under Subset Relation

Informal description

The relation "membership in a filter" is transitive with respect to the subset relation. That is, for any filter $F$ on a type $\alpha$ and sets $s, t \subseteq \alpha$, if $s \in F$ and $s \subseteq t$, then $t \in F$.

Filter.inter_mem_iff theorem

{s t : Set α} : s ∩ t ∈ f ↔ s ∈ f ∧ t ∈ f

Full source

@[simp]
theorem inter_mem_iff {s t : Set α} : s ∩ ts ∩ t ∈ fs ∩ t ∈ f ↔ s ∈ f ∧ t ∈ f :=
  ⟨fun h => ⟨mem_of_superset h inter_subset_left, mem_of_superset h inter_subset_right⟩,
    and_imp.2 inter_mem⟩

Intersection Membership Criterion for Filters: $s \cap t \in f \leftrightarrow s \in f \land t \in f$

Informal description

For any filter $f$ on a type $\alpha$ and any two subsets $s, t \subseteq \alpha$, the intersection $s \cap t$ belongs to $f$ if and only if both $s$ and $t$ belong to $f$.

Filter.diff_mem theorem

{s t : Set α} (hs : s ∈ f) (ht : tᶜ ∈ f) : s \ t ∈ f

Full source

theorem diff_mem {s t : Set α} (hs : s ∈ f) (ht : tᶜtᶜ ∈ f) : s \ ts \ t ∈ f :=
  inter_mem hs ht

Filter Membership of Set Difference under Complement Condition

Informal description

For any filter $f$ on a type $\alpha$ and any two sets $s, t \subseteq \alpha$, if $s$ belongs to $f$ and the complement $t^c$ belongs to $f$, then the set difference $s \setminus t$ also belongs to $f$.

Filter.congr_sets theorem

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

Full source

theorem congr_sets (h : { x | x ∈ s ↔ x ∈ t }{ x | x ∈ s ↔ x ∈ t } ∈ f) : s ∈ fs ∈ f ↔ t ∈ f :=
  ⟨fun hs => mp_mem hs (mem_of_superset h fun _ => Iff.mp), fun hs =>
    mp_mem hs (mem_of_superset h fun _ => Iff.mpr)⟩

Filter Membership Equivalence under Pointwise Equivalence Condition

Informal description

For any filter $f$ on a type $\alpha$ and any subsets $s, t \subseteq \alpha$, if the set $\{x \mid x \in s \leftrightarrow x \in t\}$ belongs to $f$, then $s$ belongs to $f$ if and only if $t$ belongs to $f$.

Filter.copy_eq theorem

{S} (hmem : ∀ s, s ∈ S ↔ s ∈ f) : f.copy S hmem = f

Full source

lemma copy_eq {S} (hmem : ∀ s, s ∈ Ss ∈ S ↔ s ∈ f) : f.copy S hmem = f := Filter.ext hmem

Filter Copy Equality under Equivalent Membership Conditions

Informal description

Given a filter $f$ on a type $\alpha$ and a collection of subsets $S \subseteq \mathcal{P}(\alpha)$ such that for every subset $s \subseteq \alpha$, $s \in S$ if and only if $s \in f$, then the filter copy $f.copy\ S$ is equal to $f$.

Filter.biInter_mem' theorem

 {β : Type v} {s : β → Set α} {is : Set β} (hf : is.Subsingleton) : (⋂ i ∈ is, s i) ∈ f ↔ ∀ i ∈ is, s i ∈ f

Full source

/-- Weaker version of `Filter.biInter_mem` that assumes `Subsingleton β` rather than `Finite β`. -/
theorem biInter_mem' {β : Type v} {s : β → Set α} {is : Set β} (hf : is.Subsingleton) :
    (⋂ i ∈ is, s i) ∈ f(⋂ i ∈ is, s i) ∈ f ↔ ∀ i ∈ is, s i ∈ f := by
  apply Subsingleton.induction_on hf <;> simp

Intersection of a Subsingleton Family Belongs to Filter if and only if Each Member Does

Informal description

Let $f$ be a filter on a type $\alpha$, $\beta$ be a type, $s : \beta \to \text{Set } \alpha$ be a family of sets indexed by $\beta$, and $is \subseteq \beta$ be a subsingleton set (i.e., $is$ contains at most one element). Then the intersection $\bigcap_{i \in is} s(i)$ belongs to $f$ if and only if for every $i \in is$, the set $s(i)$ belongs to $f$.

Filter.iInter_mem' theorem

{β : Sort v} {s : β → Set α} [Subsingleton β] : (⋂ i, s i) ∈ f ↔ ∀ i, s i ∈ f

Full source

/-- Weaker version of `Filter.iInter_mem` that assumes `Subsingleton β` rather than `Finite β`. -/
theorem iInter_mem' {β : Sort v} {s : β → Set α} [Subsingleton β] :
    (⋂ i, s i) ∈ f(⋂ i, s i) ∈ f ↔ ∀ i, s i ∈ f := by
  rw [← sInter_range, sInter_eq_biInter, biInter_mem' (subsingleton_range s), forall_mem_range]

Intersection of a Subsingleton Family Belongs to Filter if and only if Each Member Does

Informal description

Let $f$ be a filter on a type $\alpha$, and let $\beta$ be a subsingleton type (i.e., all elements of $\beta$ are equal). For any family of sets $s : \beta \to \text{Set } \alpha$, the intersection $\bigcap_{i} s(i)$ belongs to $f$ if and only if $s(i) \in f$ for every $i \in \beta$.

Filter.exists_mem_subset_iff theorem

: (∃ t ∈ f, t ⊆ s) ↔ s ∈ f

Full source

theorem exists_mem_subset_iff : (∃ t ∈ f, t ⊆ s) ↔ s ∈ f :=
  ⟨fun ⟨_, ht, ts⟩ => mem_of_superset ht ts, fun hs => ⟨s, hs, Subset.rfl⟩⟩

Existence of Subset in Filter iff Superset Belongs to Filter

Informal description

For any filter $f$ on a type $\alpha$ and any subset $s \subseteq \alpha$, there exists a set $t \in f$ such that $t \subseteq s$ if and only if $s$ itself belongs to the filter $f$.

Filter.monotone_mem theorem

{f : Filter α} : Monotone fun s => s ∈ f

Full source

theorem monotone_mem {f : Filter α} : Monotone fun s => s ∈ f := fun _ _ hst h =>
  mem_of_superset h hst

Monotonicity of Filter Membership with Respect to Subset Inclusion

Informal description

For any filter $f$ on a type $\alpha$, the membership predicate $(\cdot \in f) : \text{Set } \alpha \to \text{Prop}$ is monotone with respect to subset inclusion. That is, if $s \subseteq t$ are subsets of $\alpha$, then $s \in f$ implies $t \in f$.

Filter.exists_mem_and_iff theorem

 {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

Full source

theorem exists_mem_and_iff {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 := by
  constructor
  · rintro ⟨⟨u, huf, hPu⟩, v, hvf, hQv⟩
    exact
      ⟨u ∩ v, inter_mem huf hvf, hP inter_subset_left hPu, hQ inter_subset_right hQv⟩
  · rintro ⟨u, huf, hPu, hQu⟩
    exact ⟨⟨u, huf, hPu⟩, u, huf, hQu⟩

Existence of Common Set in Filter for Antitone Predicates: $(\exists u \in f, P(u)) \land (\exists u \in f, Q(u)) \leftrightarrow \exists u \in f, P(u) \land Q(u)$

Informal description

Let $f$ be a filter on a type $\alpha$, and let $P, Q : \mathcal{P}(\alpha) \to \text{Prop}$ be antitone predicates on subsets of $\alpha$. Then the following are equivalent: 1. There exists a set $u \in f$ such that $P(u)$ holds, and there exists a set $u \in f$ such that $Q(u)$ holds. 2. There exists a set $u \in f$ such that both $P(u)$ and $Q(u)$ hold.

Filter.forall_in_swap theorem

{β : Type*} {p : Set α → β → Prop} : (∀ a ∈ f, ∀ (b), p a b) ↔ ∀ (b), ∀ a ∈ f, p a b

Full source

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

Swapping Universal Quantifiers over Filter Membership

Informal description

For any filter $f$ on a type $\alpha$, any type $\beta$, and any predicate $p : \text{Set } \alpha \to \beta \to \text{Prop}$, the following are equivalent: 1. For every set $a$ in $f$ and every element $b$ of $\beta$, $p(a, b)$ holds. 2. For every element $b$ of $\beta$ and every set $a$ in $f$, $p(a, b)$ holds.

Filter.mem_principal_self theorem

(s : Set α) : s ∈ 𝓟 s

Full source

theorem mem_principal_self (s : Set α) : s ∈ 𝓟 s := Subset.rfl

Self-membership in Principal Filter

Informal description

For any set $s$ of elements of type $\alpha$, the set $s$ belongs to the principal filter generated by $s$, i.e., $s \in \mathfrak{P}(s)$.

Filter.not_le theorem

: ¬f ≤ g ↔ ∃ s ∈ g, s ∉ f

Full source

protected theorem not_le : ¬f ≤ g¬f ≤ g ↔ ∃ s ∈ g, s ∉ f := by simp_rw [le_def, not_forall, exists_prop]

Non-inclusion of Filters is Equivalent to Existence of a Set in One Filter but Not the Other

Informal description

For two filters $f$ and $g$ on a type $\alpha$, the statement $\neg (f \leq g)$ is equivalent to the existence of a set $s$ such that $s \in g$ but $s \notin f$.

Filter.GenerateSets inductive

(g : Set (Set α)) : Set α → Prop

Full source

/-- `GenerateSets g s`: `s` is in the filter closure of `g`. -/
inductive GenerateSets (g : Set (Set α)) : Set α → Prop
  | basic {s : Set α} : s ∈ g → GenerateSets g s
  | univ : GenerateSets g univ
  | superset {s t : Set α} : GenerateSets g s → s ⊆ t → GenerateSets g t
  | inter {s t : Set α} : GenerateSets g s → GenerateSets g t → GenerateSets g (s ∩ t)

Filter generation rules

Informal description

The inductive predicate `GenerateSets g s` states that the set `s` is in the filter generated by the collection of sets `g`. This means `s` can be obtained from `g` through the following rules: 1. Any set in `g` is in `GenerateSets g`. 2. The entire type `α` is in `GenerateSets g`. 3. If `s₁` and `s₂` are in `GenerateSets g`, then their intersection `s₁ ∩ s₂` is also in `GenerateSets g`. 4. If `s₁` is in `GenerateSets g` and `s₁ ⊆ s₂`, then `s₂` is in `GenerateSets g`.

Filter.generate definition

(g : Set (Set α)) : Filter α

Full source

/-- `generate g` is the largest filter containing the sets `g`. -/
def generate (g : Set (Set α)) : Filter α where
  sets := {s | GenerateSets g s}
  univ_sets := GenerateSets.univ
  sets_of_superset := GenerateSets.superset
  inter_sets := GenerateSets.inter

Filter generated by a collection of sets

Informal description

Given a collection of sets $ g $ on a type $ \alpha $, the filter `generate g` is the smallest filter containing all sets in $ g $. It consists of all sets that can be obtained from $ g $ by including the entire type $ \alpha $, taking supersets of any set in $ g $, and intersecting any two sets in $ g $.

Filter.mem_generate_of_mem theorem

{s : Set <| Set α} {U : Set α} (h : U ∈ s) : U ∈ generate s

Full source

lemma mem_generate_of_mem {s : Set <| Set α} {U : Set α} (h : U ∈ s) :
    U ∈ generate s := GenerateSets.basic h

Membership in Generated Filter

Informal description

For any collection of sets $s$ on a type $\alpha$ and any set $U \in s$, the set $U$ belongs to the filter generated by $s$.

Filter.le_generate_iff theorem

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

Full source

theorem le_generate_iff {s : Set (Set α)} {f : Filter α} : f ≤ generate s ↔ s ⊆ f.sets :=
  Iff.intro (fun h _ hu => h <| GenerateSets.basic <| hu) fun h _ hu =>
    hu.recOn (fun h' => h h') univ_mem (fun _ hxy hx => mem_of_superset hx hxy) fun _ _ hx hy =>
      inter_mem hx hy

Filter Generation Criterion: $f \leq \text{generate } s \leftrightarrow s \subseteq f$

Informal description

For any collection of sets $s$ on a type $\alpha$ and any filter $f$ on $\alpha$, the filter $f$ is finer than the filter generated by $s$ if and only if every set in $s$ belongs to $f$. In other words, $f \leq \text{generate } s \leftrightarrow s \subseteq f$.

Filter.generate_singleton theorem

(s : Set α) : generate { s } = 𝓟 s

Full source

@[simp] lemma generate_singleton (s : Set α) : generate {s} = 𝓟 s :=
  le_antisymm (fun _t ht ↦ mem_of_superset (mem_generate_of_mem <| mem_singleton _) ht) <|
    le_generate_iff.2 <| singleton_subset_iff.2 Subset.rfl

Filter Generation from Singleton Set: $\text{generate } \{s\} = \mathfrak{P}(s)$

Informal description

For any set $s$ in a type $\alpha$, the filter generated by the singleton collection $\{s\}$ is equal to the principal filter $\mathfrak{P}(s)$ (the collection of all subsets of $\alpha$ containing $s$).

Filter.mkOfClosure definition

(s : Set (Set α)) (hs : (generate s).sets = s) : Filter α

Full source

/-- `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`. -/
protected def mkOfClosure (s : Set (Set α)) (hs : (generate s).sets = s) : Filter α where
  sets := s
  univ_sets := hs ▸ univ_mem
  sets_of_superset := hs ▸ mem_of_superset
  inter_sets := hs ▸ inter_mem

Filter construction from a generating set with closure property

Informal description

Given a collection of sets $ s $ on a type $ \alpha $ and a proof $ hs $ that the sets of the filter generated by $ s $ are exactly $ s $, the function `mkOfClosure` constructs a filter on $ \alpha $ whose sets are precisely $ s $.

Filter.mkOfClosure_sets theorem

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

Full source

theorem mkOfClosure_sets {s : Set (Set α)} {hs : (generate s).sets = s} :
    Filter.mkOfClosure s hs = generate s :=
  Filter.ext fun u =>
    show u ∈ (Filter.mkOfClosure s hs).setsu ∈ (Filter.mkOfClosure s hs).sets ↔ u ∈ (generate s).sets from hs.symm ▸ Iff.rfl

Equality of Constructed Filter and Generated Filter

Informal description

For any collection of sets $s$ on a type $\alpha$ and a proof $hs$ that the sets of the filter generated by $s$ are exactly $s$, the filter constructed by `mkOfClosure` from $s$ and $hs$ is equal to the filter generated by $s$.

Filter.giGenerate definition

(α : Type*) : @GaloisInsertion (Set (Set α)) (Filter α)ᵒᵈ _ _ Filter.generate Filter.sets

Full source

/-- Galois insertion from sets of sets into filters. -/
def giGenerate (α : Type*) :
    @GaloisInsertion (Set (Set α)) (Filter α)ᵒᵈ _ _ Filter.generate Filter.sets where
  gc _ _ := le_generate_iff
  le_l_u _ _ h := GenerateSets.basic h
  choice s hs := Filter.mkOfClosure s (le_antisymm hs <| le_generate_iff.1 <| le_rfl)
  choice_eq _ _ := mkOfClosure_sets

Galois insertion between sets of sets and filters

Informal description

The Galois insertion between the collection of sets of subsets of a type $\alpha$ and the collection of filters on $\alpha$ ordered by reverse inclusion. The lower adjoint is the filter generation function `Filter.generate`, which maps a collection of sets to the smallest filter containing it, and the upper adjoint is the function `Filter.sets`, which maps a filter to its underlying collection of sets. This forms a Galois connection where for any collection of sets $s$ and any filter $f$, $s \subseteq f$ if and only if $\text{generate } s \leq f$ (with the order on filters being reverse inclusion).

Filter.mem_inf_iff theorem

{f g : Filter α} {s : Set α} : s ∈ f ⊓ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, s = t₁ ∩ t₂

Full source

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

Characterization of Membership in Filter Infimum via Intersections

Informal description

For any filters $f$ and $g$ on a type $\alpha$ and any subset $s \subseteq \alpha$, $s$ belongs to the infimum filter $f \sqcap g$ if and only if there exist subsets $t_1 \in f$ and $t_2 \in g$ such that $s = t_1 \cap t_2$.

Filter.mem_inf_of_left theorem

{f g : Filter α} {s : Set α} (h : s ∈ f) : s ∈ f ⊓ g

Full source

theorem mem_inf_of_left {f g : Filter α} {s : Set α} (h : s ∈ f) : s ∈ f ⊓ g :=
  ⟨s, h, univ, univ_mem, (inter_univ s).symm⟩

Membership in Infimum Filter from Left Component

Informal description

For any filters $f$ and $g$ on a type $\alpha$, and any set $s \subseteq \alpha$, if $s$ belongs to $f$, then $s$ also belongs to the infimum filter $f \sqcap g$.

Filter.mem_inf_of_right theorem

{f g : Filter α} {s : Set α} (h : s ∈ g) : s ∈ f ⊓ g

Full source

theorem mem_inf_of_right {f g : Filter α} {s : Set α} (h : s ∈ g) : s ∈ f ⊓ g :=
  ⟨univ, univ_mem, s, h, (univ_inter s).symm⟩

Membership in Infimum Filter from Right Component

Informal description

For any filters $f$ and $g$ on a type $\alpha$, and any set $s \subseteq \alpha$, if $s$ belongs to $g$, then $s$ belongs to the infimum filter $f \sqcap g$.

Filter.inter_mem_inf theorem

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

Full source

theorem inter_mem_inf {α : Type u} {f g : Filter α} {s t : Set α} (hs : s ∈ f) (ht : t ∈ g) :
    s ∩ ts ∩ t ∈ f ⊓ g :=
  ⟨s, hs, t, ht, rfl⟩

Intersection of Filter Sets Belongs to Infimum Filter

Informal description

Let $f$ and $g$ be filters on a type $\alpha$, and let $s$ and $t$ be subsets of $\alpha$. If $s \in f$ and $t \in g$, then the intersection $s \cap t$ belongs to the infimum filter $f \sqcap g$.

Filter.mem_inf_of_inter theorem

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

Full source

theorem mem_inf_of_inter {f g : Filter α} {s t u : Set α} (hs : s ∈ f) (ht : t ∈ g)
    (h : s ∩ ts ∩ t ⊆ u) : u ∈ f ⊓ g :=
  mem_of_superset (inter_mem_inf hs ht) h

Upward Closure of Filter Intersections: $s \cap t \subseteq u$ implies $u \in f \sqcap g$

Informal description

Let $f$ and $g$ be filters on a type $\alpha$, and let $s, t, u$ be subsets of $\alpha$. If $s \in f$, $t \in g$, and $s \cap t \subseteq u$, then $u$ belongs to the infimum filter $f \sqcap g$.

Filter.mem_inf_iff_superset theorem

{f g : Filter α} {s : Set α} : s ∈ f ⊓ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ∩ t₂ ⊆ s

Full source

theorem mem_inf_iff_superset {f g : Filter α} {s : Set α} :
    s ∈ f ⊓ gs ∈ f ⊓ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ∩ t₂ ⊆ s :=
  ⟨fun ⟨t₁, h₁, t₂, h₂, Eq⟩ => ⟨t₁, h₁, t₂, h₂, Eq ▸ Subset.rfl⟩, fun ⟨_, h₁, _, h₂, sub⟩ =>
    mem_inf_of_inter h₁ h₂ sub⟩

Characterization of Membership in Infimum Filter via Supersets

Informal description

For any filters $f$ and $g$ on a type $\alpha$ and any subset $s$ of $\alpha$, $s$ belongs to the infimum filter $f \sqcap g$ if and only if there exist subsets $t_1 \in f$ and $t_2 \in g$ such that $t_1 \cap t_2 \subseteq s$.

Filter.instCompleteLatticeFilter instance

: CompleteLattice (Filter α)

Full source

/-- Complete lattice structure on `Filter α`. -/
instance instCompleteLatticeFilter : CompleteLattice (Filter α) where
  inf a b := min a b
  sup a b := max a b
  le_sup_left _ _ _ h := h.1
  le_sup_right _ _ _ h := h.2
  sup_le _ _ _ h₁ h₂ _ h := ⟨h₁ h, h₂ h⟩
  inf_le_left _ _ _ := mem_inf_of_left
  inf_le_right _ _ _ := mem_inf_of_right
  le_inf := fun _ _ _ h₁ h₂ _s ⟨_a, ha, _b, hb, hs⟩ => hs.symm ▸ inter_mem (h₁ ha) (h₂ hb)
  le_sSup _ _ h₁ _ h₂ := h₂ h₁
  sSup_le _ _ h₁ _ h₂ _ h₃ := h₁ _ h₃ h₂
  sInf_le _ _ h₁ _ h₂ := by rw [← Filter.sSup_lowerBounds]; exact fun _ h₃ ↦ h₃ h₁ h₂
  le_sInf _ _ h₁ _ h₂ := by rw [← Filter.sSup_lowerBounds] at h₂; exact h₂ h₁
  le_top _ _ := univ_mem'
  bot_le _ _ _ := trivial

Complete Lattice Structure on Filters

Informal description

The collection of filters on a type $\alpha$ forms a complete lattice, where the order is given by reverse inclusion of sets. In this lattice: - The infimum of two filters is the filter generated by their pairwise intersections - The supremum is their intersection - The top element is the filter containing all subsets of $\alpha$ - The bottom element is the filter containing only $\alpha$ itself

Filter.instInhabited instance

: Inhabited (Filter α)

Full source

instance : Inhabited (Filter α) := ⟨⊥⟩

Existence of a Filter on Any Type

Informal description

For any type $\alpha$, the collection of filters on $\alpha$ is inhabited, meaning there exists at least one filter on $\alpha$.

Filter.NeBot.ne theorem

{f : Filter α} (hf : NeBot f) : f ≠ ⊥

Full source

theorem NeBot.ne {f : Filter α} (hf : NeBot f) : f ≠ ⊥ := hf.ne'

Non-trivial filters are not the bottom filter

Informal description

For any non-trivial filter $f$ on a type $\alpha$, $f$ is not equal to the bottom filter $\bot$.

Filter.not_neBot theorem

{f : Filter α} : ¬f.NeBot ↔ f = ⊥

Full source

@[simp] theorem not_neBot {f : Filter α} : ¬f.NeBot¬f.NeBot ↔ f = ⊥ := neBot_iff.not_left

Characterization of Trivial Filters: $\neg(\text{NeBot } f) \leftrightarrow f = \bot$

Informal description

For any filter $f$ on a type $\alpha$, the statement that $f$ is not non-trivial is equivalent to $f$ being equal to the bottom filter $\bot$. In other words, $\neg(\text{NeBot } f) \leftrightarrow f = \bot$.

Filter.NeBot.mono theorem

{f g : Filter α} (hf : NeBot f) (hg : f ≤ g) : NeBot g

Full source

theorem NeBot.mono {f g : Filter α} (hf : NeBot f) (hg : f ≤ g) : NeBot g :=
  ⟨ne_bot_of_le_ne_bot hf.1 hg⟩

Non-trivial filters are upward-closed with respect to the filter order

Informal description

For any filters $f$ and $g$ on a type $\alpha$, if $f$ is non-trivial (i.e., $f \neq \bot$) and $f \leq g$ in the partial order of filters, then $g$ is also non-trivial.

Filter.neBot_of_le theorem

{f g : Filter α} [hf : NeBot f] (hg : f ≤ g) : NeBot g

Full source

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

Non-trivial filters are upward-closed with respect to the filter order

Informal description

For any filters $f$ and $g$ on a type $\alpha$, if $f$ is non-trivial (i.e., $f \neq \bot$) and $f \leq g$ in the partial order of filters, then $g$ is also non-trivial.

Filter.sup_neBot theorem

{f g : Filter α} : NeBot (f ⊔ g) ↔ NeBot f ∨ NeBot g

Full source

@[simp] theorem sup_neBot {f g : Filter α} : NeBotNeBot (f ⊔ g) ↔ NeBot f ∨ NeBot g := by
  simp only [neBot_iff, not_and_or, Ne, sup_eq_bot_iff]

Supremum of Filters is Non-trivial if and only if One is Non-trivial

Informal description

For any two filters $f$ and $g$ on a type $\alpha$, the supremum filter $f \sqcup g$ is non-trivial if and only if at least one of $f$ or $g$ is non-trivial.

Filter.not_disjoint_self_iff theorem

: ¬Disjoint f f ↔ f.NeBot

Full source

theorem not_disjoint_self_iff : ¬Disjoint f f¬Disjoint f f ↔ f.NeBot := by rw [disjoint_self, neBot_iff]

Non-disjointness of a filter with itself characterizes non-trivial filters: $\neg \text{Disjoint}(f, f) \leftrightarrow f \text{ is non-trivial}$

Informal description

For any filter $f$ on a type $\alpha$, the filter $f$ is not disjoint from itself if and only if $f$ is non-trivial (i.e., $f \neq \bot$).

Filter.bot_sets_eq theorem

: (⊥ : Filter α).sets = univ

Full source

theorem bot_sets_eq : (⊥ : Filter α).sets = univ := rfl

Bottom Filter Contains All Subsets

Informal description

The collection of sets in the bottom filter $\bot$ on a type $\alpha$ is equal to the universal set $\text{univ}$ (the set of all subsets of $\alpha$).

Filter.sup_sets_eq theorem

{f g : Filter α} : (f ⊔ g).sets = f.sets ∩ g.sets

Full source

theorem sup_sets_eq {f g : Filter α} : (f ⊔ g).sets = f.sets ∩ g.sets :=
  (giGenerate α).gc.u_inf

Supremum Filter's Sets as Intersection of Component Filters' Sets

Informal description

For any two filters $f$ and $g$ on a type $\alpha$, the collection of sets in the supremum filter $f \sqcup g$ is equal to the intersection of the collections of sets in $f$ and $g$, i.e., $(f \sqcup g).\text{sets} = f.\text{sets} \cap g.\text{sets}$.

Filter.sSup_sets_eq theorem

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

Full source

theorem sSup_sets_eq {s : Set (Filter α)} : (sSup s).sets = ⋂ f ∈ s, (f : Filter α).sets :=
  (giGenerate α).gc.u_sInf

Supremum Filter Characterization via Intersection of Filter Sets

Informal description

For any collection $s$ of filters on a type $\alpha$, the sets in the supremum filter $\bigsqcup s$ are precisely the intersection of all sets in each filter $f \in s$. In other words, a set belongs to $\bigsqcup s$ if and only if it belongs to every filter in $s$.

Filter.iSup_sets_eq theorem

{f : ι → Filter α} : (iSup f).sets = ⋂ i, (f i).sets

Full source

theorem iSup_sets_eq {f : ι → Filter α} : (iSup f).sets = ⋂ i, (f i).sets :=
  (giGenerate α).gc.u_iInf

Supremum Filter Characterization via Intersection of Component Filters' Sets

Informal description

For any indexed family of filters $(f_i)_{i \in \iota}$ on a type $\alpha$, the collection of sets in the supremum filter $\bigsqcup_i f_i$ is equal to the intersection of the collections of sets in each $f_i$, i.e., \[ \left(\bigsqcup_i f_i\right).\text{sets} = \bigcap_i (f_i.\text{sets}). \]

Filter.generate_empty theorem

: Filter.generate ∅ = (⊤ : Filter α)

Full source

theorem generate_empty : Filter.generate ∅ = (⊤ : Filter α) :=
  (giGenerate α).gc.l_bot

Empty Set Generates Top Filter

Informal description

The filter generated by the empty collection of sets is equal to the top filter (the filter containing all subsets of the type $\alpha$).

Filter.generate_univ theorem

: Filter.generate univ = (⊥ : Filter α)

Full source

theorem generate_univ : Filter.generate univ = (⊥ : Filter α) :=
  bot_unique fun _ _ => GenerateSets.basic (mem_univ _)

Universal Set Generates Bottom Filter

Informal description

The filter generated by the universal set on a type $\alpha$ is equal to the bottom element of the lattice of filters on $\alpha$, i.e., $\text{generate}(\text{univ}) = \bot$.

Filter.generate_union theorem

{s t : Set (Set α)} : Filter.generate (s ∪ t) = Filter.generate s ⊓ Filter.generate t

Full source

theorem generate_union {s t : Set (Set α)} :
    Filter.generate (s ∪ t) = Filter.generateFilter.generate s ⊓ Filter.generate t :=
  (giGenerate α).gc.l_sup

Filter Generation of Union Equals Infimum of Generated Filters

Informal description

For any two collections of sets $s$ and $t$ on a type $\alpha$, the filter generated by their union $s \cup t$ is equal to the infimum (meet) of the filters generated by $s$ and $t$ individually, i.e., \[ \text{generate}(s \cup t) = \text{generate}(s) \sqcap \text{generate}(t). \]

Filter.generate_iUnion theorem

{s : ι → Set (Set α)} : Filter.generate (⋃ i, s i) = ⨅ i, Filter.generate (s i)

Full source

theorem generate_iUnion {s : ι → Set (Set α)} :
    Filter.generate (⋃ i, s i) = ⨅ i, Filter.generate (s i) :=
  (giGenerate α).gc.l_iSup

Filter Generation of Union Equals Infimum of Generated Filters

Informal description

For any indexed family of collections of sets $\{s_i\}_{i \in \iota}$ on a type $\alpha$, the filter generated by the union $\bigcup_i s_i$ equals the infimum of the filters generated by each individual collection $s_i$. In other words: $$\text{generate}\left(\bigcup_{i} s_i\right) = \bigsqcap_i \text{generate}(s_i)$$

Filter.mem_sup theorem

{f g : Filter α} {s : Set α} : s ∈ f ⊔ g ↔ s ∈ f ∧ s ∈ g

Full source

@[simp]
theorem mem_sup {f g : Filter α} {s : Set α} : s ∈ f ⊔ gs ∈ f ⊔ g ↔ s ∈ f ∧ s ∈ g :=
  Iff.rfl

Membership in Supremum of Two Filters

Informal description

For any filters $F$ and $G$ on a type $\alpha$ and any subset $s \subseteq \alpha$, $s$ belongs to the supremum filter $F \sqcup G$ if and only if $s$ belongs to both $F$ and $G$.

Filter.union_mem_sup theorem

{f g : Filter α} {s t : Set α} (hs : s ∈ f) (ht : t ∈ g) : s ∪ t ∈ f ⊔ g

Full source

theorem union_mem_sup {f g : Filter α} {s t : Set α} (hs : s ∈ f) (ht : t ∈ g) : s ∪ ts ∪ t ∈ f ⊔ g :=
  ⟨mem_of_superset hs subset_union_left, mem_of_superset ht subset_union_right⟩

Union of Sets from Two Filters Belongs to Their Supremum

Informal description

For any filters $f$ and $g$ on a type $\alpha$, and any subsets $s, t \subseteq \alpha$, if $s \in f$ and $t \in g$, then the union $s \cup t$ belongs to the supremum filter $f \sqcup g$.

Filter.iSup_neBot theorem

{f : ι → Filter α} : (⨆ i, f i).NeBot ↔ ∃ i, (f i).NeBot

Full source

@[simp]
theorem iSup_neBot {f : ι → Filter α} : (⨆ i, f i).NeBot ↔ ∃ i, (f i).NeBot := by
  simp [neBot_iff]

Non-triviality of Filter Supremum $\bigsqcup_i f_i \neq \bot \leftrightarrow \exists i, f_i \neq \bot$

Informal description

For a family of filters $\{f_i\}_{i \in \iota}$ on a type $\alpha$, the supremum filter $\bigsqcup_i f_i$ is non-trivial (i.e., does not contain the empty set) if and only if there exists some index $i$ for which the filter $f_i$ is non-trivial.

Filter.iInf_eq_generate theorem

(s : ι → Filter α) : iInf s = generate (⋃ i, (s i).sets)

Full source

theorem iInf_eq_generate (s : ι → Filter α) : iInf s = generate (⋃ i, (s i).sets) :=
  eq_of_forall_le_iff fun _ ↦ by simp [le_generate_iff]

Infimum of Filters as Generated by Union of Their Sets

Informal description

For any indexed family of filters $(f_i)_{i \in \iota}$ on a type $\alpha$, the infimum of the family $\bigsqcap_i f_i$ is equal to the filter generated by the union of all sets in the filters $f_i$, i.e., $\mathrm{generate}\left(\bigcup_i (f_i).\mathrm{sets}\right)$.

Filter.mem_iInf_of_mem theorem

{f : ι → Filter α} (i : ι) {s} (hs : s ∈ f i) : s ∈ ⨅ i, f i

Full source

theorem mem_iInf_of_mem {f : ι → Filter α} (i : ι) {s} (hs : s ∈ f i) : s ∈ ⨅ i, f i :=
  iInf_le f i hs

Membership Preservation under Infimum of Filters: $s \in f(i) \implies s \in \bigsqcap_i f(i)$

Informal description

For any indexed family of filters $f : \iota \to \text{Filter}(\alpha)$ on a type $\alpha$, if a set $s$ belongs to the filter $f(i)$ for some index $i \in \iota$, then $s$ also belongs to the infimum filter $\bigsqcap_i f(i)$.

Filter.le_principal_iff theorem

{s : Set α} {f : Filter α} : f ≤ 𝓟 s ↔ s ∈ f

Full source

@[simp]
theorem le_principal_iff {s : Set α} {f : Filter α} : f ≤ 𝓟 s ↔ s ∈ f :=
  ⟨fun h => h Subset.rfl, fun hs _ ht => mem_of_superset hs ht⟩

Characterization of Filter Inclusion in Principal Filter

Informal description

For any filter $f$ on a type $\alpha$ and any subset $s \subseteq \alpha$, the filter $f$ is less than or equal to the principal filter generated by $s$ if and only if $s$ is an element of $f$. In other words, $f \leq \mathfrak{P}(s) \leftrightarrow s \in f$, where $\mathfrak{P}(s)$ denotes the principal filter generated by $s$.

Filter.Iic_principal theorem

(s : Set α) : Iic (𝓟 s) = {l | s ∈ l}

Full source

theorem Iic_principal (s : Set α) : Iic (𝓟 s) = { l | s ∈ l } :=
  Set.ext fun _ => le_principal_iff

Characterization of Filters Below Principal Filter: $\text{Iic}(\mathfrak{P}(s)) = \{l \mid s \in l\}$

Informal description

For any subset $s$ of a type $\alpha$, the left-infinite right-closed interval $\text{Iic}(\mathfrak{P}(s))$ in the partial order of filters on $\alpha$ is equal to the collection of all filters $l$ that contain $s$. Here, $\mathfrak{P}(s)$ denotes the principal filter generated by $s$. In other words, the set of all filters $l$ such that $l \leq \mathfrak{P}(s)$ is exactly the set of filters that contain $s$ as an element.

Filter.principal_mono theorem

{s t : Set α} : 𝓟 s ≤ 𝓟 t ↔ s ⊆ t

Full source

theorem principal_mono {s t : Set α} : 𝓟𝓟 s ≤ 𝓟 t ↔ s ⊆ t := by
  simp only [le_principal_iff, mem_principal]

Principal Filter Monotonicity: $\mathfrak{P}(s) \leq \mathfrak{P}(t) \leftrightarrow s \subseteq t$

Informal description

For any two sets $s$ and $t$ in a type $\alpha$, the principal filter generated by $s$ is less than or equal to the principal filter generated by $t$ if and only if $s$ is a subset of $t$. In other words, $\{ U \mid s \subseteq U \} \subseteq \{ U \mid t \subseteq U \}$ if and only if $s \subseteq t$.

Filter.monotone_principal theorem

: Monotone (𝓟 : Set α → Filter α)

Full source

@[mono]
theorem monotone_principal : Monotone (𝓟 : Set α → Filter α) := fun _ _ => principal_mono.2

Monotonicity of the Principal Filter Construction

Informal description

The function that maps a set $s$ in a type $\alpha$ to the principal filter $\mathfrak{P}(s)$ is monotone with respect to the subset relation. That is, for any sets $s, t \subseteq \alpha$, if $s \subseteq t$, then $\mathfrak{P}(s) \leq \mathfrak{P}(t)$.

Filter.principal_eq_iff_eq theorem

{s t : Set α} : 𝓟 s = 𝓟 t ↔ s = t

Full source

@[simp] theorem principal_eq_iff_eq {s t : Set α} : 𝓟𝓟 s = 𝓟 t ↔ s = t := by
  simp only [le_antisymm_iff, le_principal_iff, mem_principal]; rfl

Equality of Principal Filters is Equivalent to Equality of Generating Sets

Informal description

For any two sets $s$ and $t$ in a type $\alpha$, the principal filters generated by $s$ and $t$ are equal if and only if the sets themselves are equal, i.e., $\mathfrak{P}(s) = \mathfrak{P}(t) \leftrightarrow s = t$.

Filter.join_principal_eq_sSup theorem

{s : Set (Filter α)} : join (𝓟 s) = sSup s

Full source

@[simp] theorem join_principal_eq_sSup {s : Set (Filter α)} : join (𝓟 s) = sSup s := rfl

Join of Principal Filter Equals Supremum

Informal description

For any collection $s$ of filters on a type $\alpha$, the join of the principal filter generated by $s$ is equal to the supremum of $s$ in the lattice of filters. In other words, $\text{join}(\mathfrak{P}(s)) = \sup s$.

Filter.principal_univ theorem

: 𝓟 (univ : Set α) = ⊤

Full source

@[simp] theorem principal_univ : 𝓟 (univ : Set α) = ⊤ :=
  top_unique <| by simp only [le_principal_iff, mem_top, eq_self_iff_true]

Principal Filter of Universal Set Equals Top Filter

Informal description

The principal filter generated by the universal set $\text{univ}$ on a type $\alpha$ is equal to the top element $\top$ in the lattice of filters on $\alpha$. In other words, $\mathfrak{P}(\text{univ}) = \top$.

Filter.principal_empty theorem

: 𝓟 (∅ : Set α) = ⊥

Full source

@[simp]
theorem principal_empty : 𝓟 (∅ : Set α) = ⊥ :=
  bot_unique fun _ _ => empty_subset _

Principal Filter of Empty Set is Bottom Element

Informal description

The principal filter generated by the empty set is equal to the bottom element of the filter lattice, i.e., $\mathfrak{P}(\emptyset) = \bot$.

Filter.generate_eq_biInf theorem

(S : Set (Set α)) : generate S = ⨅ s ∈ S, 𝓟 s

Full source

theorem generate_eq_biInf (S : Set (Set α)) : generate S = ⨅ s ∈ S, 𝓟 s :=
  eq_of_forall_le_iff fun f => by simp [le_generate_iff, le_principal_iff, subset_def]

Filter Generation as Infimum of Principal Filters

Informal description

For any collection of sets $S$ on a type $\alpha$, the filter generated by $S$ is equal to the infimum of the principal filters $\mathfrak{P}(s)$ for all $s \in S$. In other words, the smallest filter containing all sets in $S$ is the greatest lower bound of the principal filters generated by each individual set in $S$.

Filter.empty_mem_iff_bot theorem

{f : Filter α} : ∅ ∈ f ↔ f = ⊥

Full source

theorem empty_mem_iff_bot {f : Filter α} : ∅∅ ∈ f∅ ∈ f ↔ f = ⊥ :=
  ⟨fun h => bot_unique fun s _ => mem_of_superset h (empty_subset s), fun h => h.symm ▸ mem_bot⟩

Empty Set Membership Criterion for Bottom Filter: $\emptyset \in f \leftrightarrow f = \bot$

Informal description

For any filter $f$ on a type $\alpha$, the empty set $\emptyset$ belongs to $f$ if and only if $f$ is equal to the bottom filter $\bot$ (which contains all subsets of $\alpha$).

Filter.nonempty_of_mem theorem

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

Full source

theorem nonempty_of_mem {f : Filter α} [hf : NeBot f] {s : Set α} (hs : s ∈ f) : s.Nonempty :=
  s.eq_empty_or_nonempty.elim (fun h => absurd hs (h.symm ▸ mt empty_mem_iff_bot.mp hf.1)) id

Non-trivial Filters Contain Only Nonempty Sets

Informal description

For any non-trivial filter $f$ on a type $\alpha$ (i.e., $f \neq \bot$) and any set $s \in f$, the set $s$ is nonempty. In other words, if $s$ belongs to a non-trivial filter, then there exists some element $x \in \alpha$ such that $x \in s$.

Filter.NeBot.nonempty_of_mem theorem

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

Full source

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

Nonempty Sets in Non-trivial Filters

Informal description

For any non-trivial filter $f$ on a type $\alpha$ and any set $s$ belonging to $f$, the set $s$ is nonempty. In other words, if $f$ is non-trivial (i.e., $f \neq \bot$) and $s \in f$, then there exists an element $x \in \alpha$ such that $x \in s$.

Filter.empty_not_mem theorem

(f : Filter α) [NeBot f] : ¬∅ ∈ f

Full source

@[simp]
theorem empty_not_mem (f : Filter α) [NeBot f] : ¬∅ ∈ f := fun h => (nonempty_of_mem h).ne_empty rfl

Non-trivial Filters Do Not Contain the Empty Set

Informal description

For any non-trivial filter $f$ on a type $\alpha$, the empty set $\emptyset$ does not belong to $f$.

Filter.nonempty_of_neBot theorem

(f : Filter α) [NeBot f] : Nonempty α

Full source

theorem nonempty_of_neBot (f : Filter α) [NeBot f] : Nonempty α :=
  nonempty_of_exists <| nonempty_of_mem (univ_mem : univuniv ∈ f)

Non-trivial filters imply nonempty base type

Informal description

For any non-trivial filter $f$ on a type $\alpha$ (i.e., $f \neq \bot$), the type $\alpha$ is nonempty. In other words, there exists at least one element in $\alpha$.

Filter.compl_not_mem theorem

{f : Filter α} {s : Set α} [NeBot f] (h : s ∈ f) : sᶜ ∉ f

Full source

theorem compl_not_mem {f : Filter α} {s : Set α} [NeBot f] (h : s ∈ f) : sᶜsᶜ ∉ f := fun hsc =>
  (nonempty_of_mem (inter_mem h hsc)).ne_empty <| inter_compl_self s

Complement Set Not in Non-trivial Filter

Informal description

For any non-trivial filter $f$ on a type $\alpha$ and any set $s \in f$, the complement $s^c$ does not belong to $f$.

Filter.filter_eq_bot_of_isEmpty theorem

[IsEmpty α] (f : Filter α) : f = ⊥

Full source

theorem filter_eq_bot_of_isEmpty [IsEmpty α] (f : Filter α) : f = ⊥ :=
  empty_mem_iff_bot.mp <| univ_mem' isEmptyElim

Filters on Empty Types are Trivial

Informal description

For any type $\alpha$ that is empty (i.e., has no elements), every filter $f$ on $\alpha$ is equal to the bottom filter $\bot$.

Filter.disjoint_iff theorem

{f g : Filter α} : Disjoint f g ↔ ∃ s ∈ f, ∃ t ∈ g, Disjoint s t

Full source

protected lemma disjoint_iff {f g : Filter α} : DisjointDisjoint f g ↔ ∃ s ∈ f, ∃ t ∈ g, Disjoint s t := by
  simp only [disjoint_iff, ← empty_mem_iff_bot, mem_inf_iff, inf_eq_inter, bot_eq_empty,
    @eq_comm _ ∅]

Disjointness of Filters via Disjoint Sets

Informal description

Two filters $f$ and $g$ on a type $\alpha$ are disjoint if and only if there exist sets $s \in f$ and $t \in g$ such that $s$ and $t$ are disjoint.

Filter.disjoint_of_disjoint_of_mem theorem

{f g : Filter α} {s t : Set α} (h : Disjoint s t) (hs : s ∈ f) (ht : t ∈ g) : Disjoint f g

Full source

theorem disjoint_of_disjoint_of_mem {f g : Filter α} {s t : Set α} (h : Disjoint s t) (hs : s ∈ f)
    (ht : t ∈ g) : Disjoint f g :=
  Filter.disjoint_iff.mpr ⟨s, hs, t, ht, h⟩

Disjoint Filters via Disjoint Sets

Informal description

For any two filters $f$ and $g$ on a type $\alpha$, if there exist sets $s \in f$ and $t \in g$ that are disjoint, then the filters $f$ and $g$ themselves are disjoint.

Filter.NeBot.not_disjoint theorem

(hf : f.NeBot) (hs : s ∈ f) (ht : t ∈ f) : ¬Disjoint s t

Full source

theorem NeBot.not_disjoint (hf : f.NeBot) (hs : s ∈ f) (ht : t ∈ f) : ¬Disjoint s t := fun h =>
  not_disjoint_self_iff.2 hf <| Filter.disjoint_iff.2 ⟨s, hs, t, ht, h⟩

Non-disjointness of Sets in a Non-trivial Filter

Informal description

For a non-trivial filter $f$ on a type $\alpha$ (i.e., $f \neq \bot$), and any two sets $s, t \in f$, the sets $s$ and $t$ cannot be disjoint.

Filter.inf_eq_bot_iff theorem

{f g : Filter α} : f ⊓ g = ⊥ ↔ ∃ U ∈ f, ∃ V ∈ g, U ∩ V = ∅

Full source

theorem inf_eq_bot_iff {f g : Filter α} : f ⊓ gf ⊓ g = ⊥ ↔ ∃ U ∈ f, ∃ V ∈ g, U ∩ V = ∅ := by
  simp only [← disjoint_iff, Filter.disjoint_iff, Set.disjoint_iff_inter_eq_empty]

Characterization of Disjoint Filters via Infimum and Empty Intersection

Informal description

For any two filters $f$ and $g$ on a type $\alpha$, their infimum $f \sqcap g$ is equal to the bottom filter $\bot$ if and only if there exist sets $U \in f$ and $V \in g$ such that $U \cap V = \emptyset$.

Filter.unique instance

[IsEmpty α] : Unique (Filter α)

Full source

/-- There is exactly one filter on an empty type. -/
instance unique [IsEmpty α] : Unique (Filter α) where
  default := ⊥
  uniq := filter_eq_bot_of_isEmpty

Unique Filter on Empty Types

Informal description

For any empty type $\alpha$, there is exactly one filter on $\alpha$, which is the unique filter in the lattice of filters on $\alpha$.

Filter.NeBot.nonempty theorem

(f : Filter α) [hf : f.NeBot] : Nonempty α

Full source

theorem NeBot.nonempty (f : Filter α) [hf : f.NeBot] : Nonempty α :=
  not_isEmpty_iff.mp fun _ ↦ hf.ne (Subsingleton.elim _ _)

Non-trivial filters imply nonempty base type

Informal description

For any non-trivial filter $f$ on a type $\alpha$, the type $\alpha$ is nonempty.

Filter.forall_mem_nonempty_iff_neBot theorem

{f : Filter α} : (∀ s : Set α, s ∈ f → s.Nonempty) ↔ NeBot f

Full source

theorem forall_mem_nonempty_iff_neBot {f : Filter α} :
    (∀ s : Set α, s ∈ f → s.Nonempty) ↔ NeBot f :=
  ⟨fun h => ⟨fun hf => not_nonempty_empty (h ∅ <| hf.symm ▸ mem_bot)⟩, @nonempty_of_mem _ _⟩

Characterization of Non-trivial Filters via Nonempty Sets

Informal description

For any filter $f$ on a type $\alpha$, the following are equivalent: 1. Every set $s$ in $f$ is nonempty. 2. The filter $f$ is non-trivial (i.e., $f \neq \bot$).

Filter.instNeBotTop instance

[Nonempty α] : NeBot (⊤ : Filter α)

Full source

instance instNeBotTop [Nonempty α] : NeBot (⊤ : Filter α) :=
  forall_mem_nonempty_iff_neBot.1 fun s hs => by rwa [mem_top.1 hs, ← nonempty_iff_univ_nonempty]

Non-triviality of the Top Filter on Nonempty Types

Informal description

For any nonempty type $\alpha$, the top filter $\top$ on $\alpha$ (which consists of all subsets of $\alpha$) is non-trivial.

Filter.instNontrivialFilter instance

[Nonempty α] : Nontrivial (Filter α)

Full source

instance instNontrivialFilter [Nonempty α] : Nontrivial (Filter α) :=
  ⟨⟨⊤, ⊥, instNeBotTop.ne⟩⟩

Nontriviality of the Filter Lattice on Nonempty Types

Informal description

For any nonempty type $\alpha$, the collection of filters on $\alpha$ is a nontrivial type, meaning it contains at least two distinct filters.

Filter.nontrivial_iff_nonempty theorem

: Nontrivial (Filter α) ↔ Nonempty α

Full source

theorem nontrivial_iff_nonempty : NontrivialNontrivial (Filter α) ↔ Nonempty α :=
  ⟨fun _ =>
    by_contra fun h' =>
      haveI := not_nonempty_iff.1 h'
      not_subsingleton (Filter α) inferInstance,
    @Filter.instNontrivialFilter α⟩

Nontriviality of Filter Lattice Equivalent to Nonemptiness of Type

Informal description

The collection of filters on a type $\alpha$ is nontrivial (contains at least two distinct filters) if and only if $\alpha$ is nonempty.

Filter.iInf_sets_eq theorem

{f : ι → Filter α} (h : Directed (· ≥ ·) f) [ne : Nonempty ι] : (iInf f).sets = ⋃ i, (f i).sets

Full source

theorem iInf_sets_eq {f : ι → Filter α} (h : Directed (· ≥ ·) f) [ne : Nonempty ι] :
    (iInf f).sets = ⋃ i, (f i).sets :=
  let ⟨i⟩ := ne
  let u :=
    { sets := ⋃ i, (f i).sets
      univ_sets := mem_iUnion.2 ⟨i, univ_mem⟩
      sets_of_superset := by
        simp only [mem_iUnion, exists_imp]
        exact fun i hx hxy => ⟨i, mem_of_superset hx hxy⟩
      inter_sets := by
        simp only [mem_iUnion, exists_imp]
        intro x y a hx b hy
        rcases h a b with ⟨c, ha, hb⟩
        exact ⟨c, inter_mem (ha hx) (hb hy)⟩ }
  have : u = iInf f := eq_iInf_of_mem_iff_exists_mem mem_iUnion
  congr_arg Filter.sets this.symm

Infimum Filter Sets as Union of Directed Family of Filters

Informal description

For a directed family of filters $\{f_i\}_{i \in \iota}$ on a type $\alpha$ (with respect to the reverse inclusion order $\supseteq$) and a nonempty index set $\iota$, the sets of the infimum filter $\bigsqcap_i f_i$ are equal to the union of the sets of the individual filters $f_i$, i.e., \[ \left(\bigsqcap_i f_i\right).\text{sets} = \bigcup_i (f_i).\text{sets}. \]

Filter.mem_iInf_of_directed theorem

{f : ι → Filter α} (h : Directed (· ≥ ·) f) [Nonempty ι] (s) : s ∈ iInf f ↔ ∃ i, s ∈ f i

Full source

theorem mem_iInf_of_directed {f : ι → Filter α} (h : Directed (· ≥ ·) f) [Nonempty ι] (s) :
    s ∈ iInf fs ∈ iInf f ↔ ∃ i, s ∈ f i := by
  simp only [← Filter.mem_sets, iInf_sets_eq h, mem_iUnion]

Characterization of Membership in Infimum of Directed Family of Filters

Informal description

For a directed family of filters $\{f_i\}_{i \in \iota}$ on a type $\alpha$ (with respect to the reverse inclusion order $\supseteq$) and a nonempty index set $\iota$, a set $s$ belongs to the infimum filter $\bigsqcap_i f_i$ if and only if there exists an index $i$ such that $s$ belongs to $f_i$. In other words: \[ s \in \bigsqcap_i f_i \leftrightarrow \exists i, s \in f_i. \]

Filter.mem_biInf_of_directed theorem

 {f : β → Filter α} {s : Set β} (h : DirectedOn (f ⁻¹'o (· ≥ ·)) s) (ne : s.Nonempty) {t : Set α} :
  (t ∈ ⨅ i ∈ s, f i) ↔ ∃ i ∈ s, t ∈ f i

Full source

theorem mem_biInf_of_directed {f : β → Filter α} {s : Set β} (h : DirectedOn (f ⁻¹'o (· ≥ ·)) s)
    (ne : s.Nonempty) {t : Set α} : (t ∈ ⨅ i ∈ s, f i) ↔ ∃ i ∈ s, t ∈ f i := by
  haveI := ne.to_subtype
  simp_rw [iInf_subtype', mem_iInf_of_directed h.directed_val, Subtype.exists, exists_prop]

Characterization of Membership in Infimum of Directed Family of Filters over a Subset

Informal description

For a family of filters $\{f_i\}_{i \in \beta}$ on a type $\alpha$ and a nonempty subset $s \subseteq \beta$ such that the family is directed with respect to the reverse inclusion order $\supseteq$ on $s$, a set $t \subseteq \alpha$ belongs to the infimum filter $\bigsqcap_{i \in s} f_i$ if and only if there exists an index $i \in s$ such that $t \in f_i$. In other words: \[ t \in \bigsqcap_{i \in s} f_i \leftrightarrow \exists i \in s, t \in f_i. \]

Filter.biInf_sets_eq theorem

 {f : β → Filter α} {s : Set β} (h : DirectedOn (f ⁻¹'o (· ≥ ·)) s) (ne : s.Nonempty) :
  (⨅ i ∈ s, f i).sets = ⋃ i ∈ s, (f i).sets

Full source

theorem biInf_sets_eq {f : β → Filter α} {s : Set β} (h : DirectedOn (f ⁻¹'o (· ≥ ·)) s)
    (ne : s.Nonempty) : (⨅ i ∈ s, f i).sets = ⋃ i ∈ s, (f i).sets :=
  ext fun t => by simp [mem_biInf_of_directed h ne]

Equality of Infimum Filter Sets and Union of Directed Family Filter Sets

Informal description

Let $\{f_i\}_{i \in \beta}$ be a family of filters on a type $\alpha$, and let $s$ be a nonempty subset of $\beta$ such that the family is directed with respect to the reverse inclusion order $\supseteq$ on $s$. Then the collection of sets in the infimum filter $\bigsqcap_{i \in s} f_i$ is equal to the union of the collections of sets in each $f_i$ for $i \in s$. In symbols: \[ \left(\bigsqcap_{i \in s} f_i\right).\text{sets} = \bigcup_{i \in s} (f_i).\text{sets}. \]

Filter.sup_join theorem

{f₁ f₂ : Filter (Filter α)} : join f₁ ⊔ join f₂ = join (f₁ ⊔ f₂)

Full source

@[simp]
theorem sup_join {f₁ f₂ : Filter (Filter α)} : joinjoin f₁ ⊔ join f₂ = join (f₁ ⊔ f₂) :=
  Filter.ext fun x => by simp only [mem_sup, mem_join]

Join-Supremum Commutation for Filters: $\text{join}(f_1) ⊔ \text{join}(f_2) = \text{join}(f_1 ⊔ f_2)$

Informal description

For any two filters $f_1$ and $f_2$ on the type of filters over $\alpha$, the supremum of their joins equals the join of their supremum. In symbols: \[ \text{join}(f_1) ⊔ \text{join}(f_2) = \text{join}(f_1 ⊔ f_2) \]

Filter.iSup_join theorem

{ι : Sort w} {f : ι → Filter (Filter α)} : ⨆ x, join (f x) = join (⨆ x, f x)

Full source

@[simp]
theorem iSup_join {ι : Sort w} {f : ι → Filter (Filter α)} : ⨆ x, join (f x) = join (⨆ x, f x) :=
  Filter.ext fun x => by simp only [mem_iSup, mem_join]

Supremum of Joins Equals Join of Supremum for Filters

Informal description

For any indexed family of filters $\{f_i\}_{i \in \iota}$ on the type of filters over $\alpha$, the supremum of the joins of each $f_i$ is equal to the join of the supremum of the family $\{f_i\}_{i \in \iota}$. In symbols: \[ \bigsqcup_{i} \text{join}(f_i) = \text{join}\left(\bigsqcup_{i} f_i\right) \]

Filter.instDistribLattice instance

: DistribLattice (Filter α)

Full source

instance : DistribLattice (Filter α) :=
  { Filter.instCompleteLatticeFilter with
    le_sup_inf := by
      intro x y z s
      simp only [and_assoc, mem_inf_iff, mem_sup, exists_prop, exists_imp, and_imp]
      rintro hs t₁ ht₁ t₂ ht₂ rfl
      exact
        ⟨t₁, x.sets_of_superset hs inter_subset_left, ht₁, t₂,
          x.sets_of_superset hs inter_subset_right, ht₂, rfl⟩ }

Distributive Lattice Structure on Filters

Informal description

The collection of filters on a type $\alpha$ forms a distributive lattice, where the order is given by reverse inclusion of sets. In this lattice, the binary operations of join (least upper bound, $\sqcup$) and meet (greatest lower bound, $\sqcap$) satisfy the distributivity property: $$(x \sqcup y) \sqcap (x \sqcup z) \leq x \sqcup (y \sqcap z)$$ for all filters $x, y, z$ on $\alpha$.

Filter.iInf_neBot_of_directed' theorem

{f : ι → Filter α} [Nonempty ι] (hd : Directed (· ≥ ·) f) : (∀ i, NeBot (f i)) → NeBot (iInf f)

Full source

/-- 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 iInf_neBot_of_directed' {f : ι → Filter α} [Nonempty ι] (hd : Directed (· ≥ ·) f) :
    (∀ i, NeBot (f i)) → NeBot (iInf f) :=
  not_imp_not.1 <| by simpa only [not_forall, not_neBot, ← empty_mem_iff_bot,
    mem_iInf_of_directed hd] using id

Non-triviality of Infimum of Directed Non-trivial Filters

Informal description

Let $\{f_i\}_{i \in \iota}$ be a directed family of filters on a type $\alpha$ with respect to the reverse inclusion order $\supseteq$, where the index set $\iota$ is nonempty. If each filter $f_i$ is non-trivial (i.e., $f_i \neq \bot$ for all $i$), then the infimum filter $\bigsqcap_i f_i$ is also non-trivial.

Filter.iInf_neBot_of_directed theorem

{f : ι → Filter α} [hn : Nonempty α] (hd : Directed (· ≥ ·) f) (hb : ∀ i, NeBot (f i)) : NeBot (iInf f)

Full source

/-- 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 iInf_neBot_of_directed {f : ι → Filter α} [hn : Nonempty α] (hd : Directed (· ≥ ·) f)
    (hb : ∀ i, NeBot (f i)) : NeBot (iInf f) := by
  cases isEmpty_or_nonempty ι
  · constructor
    simp [iInf_of_empty f, top_ne_bot]
  · exact iInf_neBot_of_directed' hd hb

Non-triviality of Infimum of Directed Non-trivial Filters on Nonempty Type

Informal description

Let $\{f_i\}_{i \in \iota}$ be a directed family of filters on a nonempty type $\alpha$ with respect to the reverse inclusion order $\supseteq$. If each filter $f_i$ is non-trivial (i.e., $f_i \neq \bot$ for all $i$), then the infimum filter $\bigsqcap_i f_i$ is also non-trivial.

Filter.sInf_neBot_of_directed' theorem

{s : Set (Filter α)} (hne : s.Nonempty) (hd : DirectedOn (· ≥ ·) s) (hbot : ⊥ ∉ s) : NeBot (sInf s)

Full source

theorem sInf_neBot_of_directed' {s : Set (Filter α)} (hne : s.Nonempty) (hd : DirectedOn (· ≥ ·) s)
    (hbot : ⊥⊥ ∉ s) : NeBot (sInf s) :=
  (sInf_eq_iInf' s).symm ▸
    @iInf_neBot_of_directed' _ _ _ hne.to_subtype hd.directed_val fun ⟨_, hf⟩ =>
      ⟨ne_of_mem_of_not_mem hf hbot⟩

Non-triviality of Infimum of Directed Non-trivial Filter Set

Informal description

Let $s$ be a nonempty set of filters on a type $\alpha$, directed with respect to the reverse inclusion order $\supseteq$. If the bottom filter $\bot$ is not in $s$, then the infimum of $s$ is a non-trivial filter (i.e., $\mathrm{sInf}(s) \neq \bot$).

Filter.sInf_neBot_of_directed theorem

[Nonempty α] {s : Set (Filter α)} (hd : DirectedOn (· ≥ ·) s) (hbot : ⊥ ∉ s) : NeBot (sInf s)

Full source

theorem sInf_neBot_of_directed [Nonempty α] {s : Set (Filter α)} (hd : DirectedOn (· ≥ ·) s)
    (hbot : ⊥⊥ ∉ s) : NeBot (sInf s) :=
  (sInf_eq_iInf' s).symm ▸
    iInf_neBot_of_directed hd.directed_val fun ⟨_, hf⟩ => ⟨ne_of_mem_of_not_mem hf hbot⟩

Non-triviality of Infimum of Directed Non-trivial Filter Set on Nonempty Type

Informal description

Let $\alpha$ be a nonempty type and $s$ be a set of filters on $\alpha$. If $s$ is directed with respect to the reverse inclusion order $\supseteq$ and does not contain the bottom filter $\bot$, then the infimum of $s$ is a non-trivial filter (i.e., $\bigsqcap s \neq \bot$).

Filter.iInf_neBot_iff_of_directed' theorem

{f : ι → Filter α} [Nonempty ι] (hd : Directed (· ≥ ·) f) : NeBot (iInf f) ↔ ∀ i, NeBot (f i)

Full source

theorem iInf_neBot_iff_of_directed' {f : ι → Filter α} [Nonempty ι] (hd : Directed (· ≥ ·) f) :
    NeBotNeBot (iInf f) ↔ ∀ i, NeBot (f i) :=
  ⟨fun H i => H.mono (iInf_le _ i), iInf_neBot_of_directed' hd⟩

Non-triviality of Infimum of Directed Filters: $\bigsqcap_i f_i \neq \bot \leftrightarrow \forall i, f_i \neq \bot$

Informal description

Let $\{f_i\}_{i \in \iota}$ be a directed family of filters on a type $\alpha$ with respect to the reverse inclusion order $\supseteq$, where the index set $\iota$ is nonempty. Then the infimum filter $\bigsqcap_i f_i$ is non-trivial if and only if each filter $f_i$ is non-trivial.

Filter.iInf_neBot_iff_of_directed theorem

{f : ι → Filter α} [Nonempty α] (hd : Directed (· ≥ ·) f) : NeBot (iInf f) ↔ ∀ i, NeBot (f i)

Full source

theorem iInf_neBot_iff_of_directed {f : ι → Filter α} [Nonempty α] (hd : Directed (· ≥ ·) f) :
    NeBotNeBot (iInf f) ↔ ∀ i, NeBot (f i) :=
  ⟨fun H i => H.mono (iInf_le _ i), iInf_neBot_of_directed hd⟩

Non-triviality of Infimum of Directed Filters on Nonempty Type: $\bigsqcap_i f_i \neq \bot \leftrightarrow \forall i, f_i \neq \bot$

Informal description

Let $\{f_i\}_{i \in \iota}$ be a directed family of filters on a nonempty type $\alpha$ with respect to the reverse inclusion order $\supseteq$. Then the infimum filter $\bigsqcap_i f_i$ is non-trivial if and only if each filter $f_i$ is non-trivial.

Filter.inf_principal theorem

{s t : Set α} : 𝓟 s ⊓ 𝓟 t = 𝓟 (s ∩ t)

Full source

@[simp]
theorem inf_principal {s t : Set α} : 𝓟𝓟 s ⊓ 𝓟 t = 𝓟 (s ∩ t) :=
  le_antisymm
    (by simp only [le_principal_iff, mem_inf_iff]; exact ⟨s, Subset.rfl, t, Subset.rfl, rfl⟩)
    (by simp [le_inf_iff, inter_subset_left, inter_subset_right])

Infimum of Principal Filters is Principal Filter of Intersection

Informal description

For any two sets $s$ and $t$ in a type $\alpha$, the infimum of the principal filters generated by $s$ and $t$ is equal to the principal filter generated by their intersection. That is, \[ \mathfrak{P}(s) \sqcap \mathfrak{P}(t) = \mathfrak{P}(s \cap t), \] where $\mathfrak{P}(s)$ denotes the principal filter generated by the set $s$.

Filter.sup_principal theorem

{s t : Set α} : 𝓟 s ⊔ 𝓟 t = 𝓟 (s ∪ t)

Full source

@[simp]
theorem sup_principal {s t : Set α} : 𝓟𝓟 s ⊔ 𝓟 t = 𝓟 (s ∪ t) :=
  Filter.ext fun u => by simp only [union_subset_iff, mem_sup, mem_principal]

Supremum of Principal Filters is Principal Filter of Union

Informal description

For any two sets $s$ and $t$ in a type $\alpha$, the supremum of the principal filters generated by $s$ and $t$ is equal to the principal filter generated by their union. That is, \[ \mathfrak{P}(s) \sqcup \mathfrak{P}(t) = \mathfrak{P}(s \cup t), \] where $\mathfrak{P}(s)$ denotes the principal filter generated by the set $s$.

Filter.iSup_principal theorem

{ι : Sort w} {s : ι → Set α} : ⨆ x, 𝓟 (s x) = 𝓟 (⋃ i, s i)

Full source

@[simp]
theorem iSup_principal {ι : Sort w} {s : ι → Set α} : ⨆ x, 𝓟 (s x) = 𝓟 (⋃ i, s i) :=
  Filter.ext fun x => by simp only [mem_iSup, mem_principal, iUnion_subset_iff]

Supremum of Principal Filters Equals Principal Filter of Union

Informal description

For any indexed family of sets $\{s_i\}_{i \in \iota}$ in a type $\alpha$, the supremum of the principal filters generated by each $s_i$ is equal to the principal filter generated by their union. That is, \[ \bigsqcup_{i} \mathfrak{P}(s_i) = \mathfrak{P}\left(\bigcup_{i} s_i\right), \] where $\mathfrak{P}(s)$ denotes the principal filter generated by the set $s$.

Filter.principal_eq_bot_iff theorem

{s : Set α} : 𝓟 s = ⊥ ↔ s = ∅

Full source

@[simp]
theorem principal_eq_bot_iff {s : Set α} : 𝓟𝓟 s = ⊥ ↔ s = ∅ :=
  empty_mem_iff_bot.symm.trans <| mem_principal.trans subset_empty_iff

Principal Filter is Bottom if and only if Set is Empty: $\mathcal{P}(s) = \bot \leftrightarrow s = \emptyset$

Informal description

For any set $s$ in a type $\alpha$, the principal filter generated by $s$ is equal to the bottom filter $\bot$ if and only if $s$ is the empty set, i.e., $\mathcal{P}(s) = \bot \leftrightarrow s = \emptyset$.

Filter.principal_neBot_iff theorem

{s : Set α} : NeBot (𝓟 s) ↔ s.Nonempty

Full source

@[simp]
theorem principal_neBot_iff {s : Set α} : NeBotNeBot (𝓟 s) ↔ s.Nonempty :=
  neBot_iff.trans <| (not_congr principal_eq_bot_iff).trans nonempty_iff_ne_empty.symm

Non-triviality of Principal Filter: $\mathfrak{P}(s) \neq \bot \leftrightarrow s \neq \emptyset$

Informal description

For any set $s$ in a type $\alpha$, the principal filter $\mathfrak{P}(s)$ is non-trivial if and only if $s$ is nonempty, i.e., $\mathfrak{P}(s) \neq \bot \leftrightarrow s \neq \emptyset$.

Filter.isCompl_principal theorem

(s : Set α) : IsCompl (𝓟 s) (𝓟 sᶜ)

Full source

theorem isCompl_principal (s : Set α) : IsCompl (𝓟 s) (𝓟 sᶜ) :=
  IsCompl.of_eq (by rw [inf_principal, inter_compl_self, principal_empty]) <| by
    rw [sup_principal, union_compl_self, principal_univ]

Complementarity of Principal Filters Generated by a Set and Its Complement

Informal description

For any set $s$ in a type $\alpha$, the principal filter $\mathfrak{P}(s)$ generated by $s$ and the principal filter $\mathfrak{P}(s^c)$ generated by its complement $s^c$ are complements in the lattice of filters on $\alpha$. That is, their meet is the bottom filter and their join is the top filter: \[ \mathfrak{P}(s) \sqcap \mathfrak{P}(s^c) = \bot \quad \text{and} \quad \mathfrak{P}(s) \sqcup \mathfrak{P}(s^c) = \top. \]

Filter.mem_inf_principal' theorem

{f : Filter α} {s t : Set α} : s ∈ f ⊓ 𝓟 t ↔ tᶜ ∪ s ∈ f

Full source

theorem mem_inf_principal' {f : Filter α} {s t : Set α} : s ∈ f ⊓ 𝓟 ts ∈ f ⊓ 𝓟 t ↔ tᶜ ∪ s ∈ f := by
  simp only [← le_principal_iff, (isCompl_principal s).le_left_iff, disjoint_assoc, inf_principal,
    ← (isCompl_principal (t ∩ sᶜ)).le_right_iff, compl_inter, compl_compl]

Membership Criterion for Infimum of Filter and Principal Filter via Complement Union

Informal description

For a filter $f$ on a type $\alpha$ and sets $s, t \subseteq \alpha$, the set $s$ belongs to the infimum of $f$ and the principal filter generated by $t$ if and only if the union of the complement of $t$ with $s$ belongs to $f$, i.e., $$ s \in f \sqcap \mathfrak{P}(t) \leftrightarrow t^c \cup s \in f. $$

Filter.mem_inf_principal theorem

{f : Filter α} {s t : Set α} : s ∈ f ⊓ 𝓟 t ↔ {x | x ∈ t → x ∈ s} ∈ f

Full source

lemma mem_inf_principal {f : Filter α} {s t : Set α} : s ∈ f ⊓ 𝓟 ts ∈ f ⊓ 𝓟 t ↔ { x | x ∈ t → x ∈ s } ∈ f := by
  simp only [mem_inf_principal', imp_iff_not_or, setOf_or, compl_def, setOf_mem_eq]

Membership in Infimum of Filter and Principal Filter

Informal description

For a filter $f$ on a type $\alpha$ and sets $s, t \subseteq \alpha$, the set $s$ belongs to the infimum of $f$ and the principal filter generated by $t$ if and only if the set $\{x \mid x \in t \to x \in s\}$ belongs to $f$.

Filter.iSup_inf_principal theorem

(f : ι → Filter α) (s : Set α) : ⨆ i, f i ⊓ 𝓟 s = (⨆ i, f i) ⊓ 𝓟 s

Full source

lemma iSup_inf_principal (f : ι → Filter α) (s : Set α) : ⨆ i, f i ⊓ 𝓟 s = (⨆ i, f i) ⊓ 𝓟 s := by
  ext
  simp only [mem_iSup, mem_inf_principal]

Supremum of Filter Intersections with Principal Filter

Informal description

For any indexed family of filters $(f_i)_{i \in \iota}$ on a type $\alpha$ and any subset $s \subseteq \alpha$, the supremum of the filters $(f_i \sqcap \mathfrak{P}(s))$ equals the supremum of the $f_i$ intersected with the principal filter generated by $s$. That is, \[ \bigsqcup_{i \in \iota} (f_i \sqcap \mathfrak{P}(s)) = \left(\bigsqcup_{i \in \iota} f_i\right) \sqcap \mathfrak{P}(s). \] Here, $\mathfrak{P}(s)$ denotes the principal filter generated by $s$.

Filter.inf_principal_eq_bot theorem

{f : Filter α} {s : Set α} : f ⊓ 𝓟 s = ⊥ ↔ sᶜ ∈ f

Full source

theorem inf_principal_eq_bot {f : Filter α} {s : Set α} : f ⊓ 𝓟 sf ⊓ 𝓟 s = ⊥ ↔ sᶜ ∈ f := by
  rw [← empty_mem_iff_bot, mem_inf_principal]
  simp only [mem_empty_iff_false, imp_false, compl_def]

Infimum of Filter and Principal Filter is Bottom if and only if Complement Belongs to Filter

Informal description

For a filter $f$ on a type $\alpha$ and a subset $s \subseteq \alpha$, the infimum of $f$ and the principal filter generated by $s$ is equal to the bottom filter $\bot$ if and only if the complement of $s$ belongs to $f$. In other words: \[ f \sqcap \mathfrak{P}(s) = \bot \leftrightarrow s^c \in f. \] Here, $\mathfrak{P}(s)$ denotes the principal filter generated by $s$.

Filter.mem_of_eq_bot theorem

{f : Filter α} {s : Set α} (h : f ⊓ 𝓟 sᶜ = ⊥) : s ∈ f

Full source

theorem mem_of_eq_bot {f : Filter α} {s : Set α} (h : f ⊓ 𝓟 sᶜ = ⊥) : s ∈ f := by
  rwa [inf_principal_eq_bot, compl_compl] at h

Membership in Filter from Infimum with Principal Complement Filter Being Bottom

Informal description

Let $f$ be a filter on a type $\alpha$ and $s$ a subset of $\alpha$. If the infimum of $f$ and the principal filter generated by the complement of $s$ is equal to the bottom filter, then $s$ belongs to $f$. In other words: \[ f \sqcap \mathfrak{P}(s^c) = \bot \implies s \in f. \] Here, $\mathfrak{P}(s^c)$ denotes the principal filter generated by $s^c$.

Filter.diff_mem_inf_principal_compl theorem

{f : Filter α} {s : Set α} (hs : s ∈ f) (t : Set α) : s \ t ∈ f ⊓ 𝓟 tᶜ

Full source

theorem diff_mem_inf_principal_compl {f : Filter α} {s : Set α} (hs : s ∈ f) (t : Set α) :
    s \ ts \ t ∈ f ⊓ 𝓟 tᶜ :=
  inter_mem_inf hs <| mem_principal_self tᶜ

Set Difference in Infimum of Filter and Principal Complement Filter

Informal description

Let $f$ be a filter on a type $\alpha$, and let $s$ be a set in $f$. For any set $t \subseteq \alpha$, the set difference $s \setminus t$ belongs to the infimum filter $f \sqcap \mathfrak{P}(t^c)$, where $\mathfrak{P}(t^c)$ is the principal filter generated by the complement of $t$.

Filter.principal_le_iff theorem

{s : Set α} {f : Filter α} : 𝓟 s ≤ f ↔ ∀ V ∈ f, s ⊆ V

Full source

theorem principal_le_iff {s : Set α} {f : Filter α} : 𝓟𝓟 s ≤ f ↔ ∀ V ∈ f, s ⊆ V := by
  simp_rw [le_def, mem_principal]

Characterization of Principal Filter Inclusion: $\mathfrak{P}(s) \leq f \leftrightarrow (\forall V \in f, s \subseteq V)$

Informal description

For any set $s$ in a type $\alpha$ and any filter $f$ on $\alpha$, the principal filter $\mathfrak{P}(s)$ is less than or equal to $f$ if and only if for every set $V$ in $f$, $s$ is a subset of $V$. In other words, $\mathfrak{P}(s) \leq f \leftrightarrow (\forall V \in f, s \subseteq V)$.

Filter.join_mono theorem

{f₁ f₂ : Filter (Filter α)} (h : f₁ ≤ f₂) : join f₁ ≤ join f₂

Full source

@[mono, gcongr]
theorem join_mono {f₁ f₂ : Filter (Filter α)} (h : f₁ ≤ f₂) : join f₁ ≤ join f₂ := fun _ hs => h hs

Monotonicity of Filter Join Operation

Informal description

For any two filters of filters $f_1$ and $f_2$ on a type $\alpha$, if $f_1 \leq f_2$ (i.e., $f_1$ is finer than $f_2$), then the join of $f_1$ is finer than the join of $f_2$, i.e., $\text{join } f_1 \leq \text{join } f_2$.

Filter.eventually_iff theorem

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

Full source

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

Characterization of "Eventually" via Filter Membership

Informal description

For a filter $f$ on a type $\alpha$ and a predicate $P : \alpha \to \text{Prop}$, the statement $\forallᶠ x \text{ in } f, P x$ holds if and only if the set $\{x \mid P x\}$ belongs to the filter $f$.

Filter.eventually_mem_set theorem

{s : Set α} {l : Filter α} : (∀ᶠ x in l, x ∈ s) ↔ s ∈ l

Full source

@[simp]
theorem eventually_mem_set {s : Set α} {l : Filter α} : (∀ᶠ x in l, x ∈ s) ↔ s ∈ l :=
  Iff.rfl

Equivalence of Eventual Membership and Filter Membership

Informal description

For any set $s$ in a type $\alpha$ and any filter $l$ on $\alpha$, the property that $x$ belongs to $s$ holds eventually with respect to $l$ if and only if $s$ is an element of the filter $l$. In other words, $\forallᶠ x \text{ in } l, x \in s \leftrightarrow s \in l$.

Filter.ext' theorem

{f₁ f₂ : Filter α} (h : ∀ p : α → Prop, (∀ᶠ x in f₁, p x) ↔ ∀ᶠ x in f₂, p x) : f₁ = f₂

Full source

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

Extensionality of Filters via Eventual Properties

Informal description

For any two filters $f_1$ and $f_2$ on a type $\alpha$, if for every predicate $p : \alpha \to \text{Prop}$ the property $p$ holds eventually in $f_1$ if and only if it holds eventually in $f_2$, then $f_1 = f_2$.

Filter.Eventually.filter_mono theorem

{f₁ f₂ : Filter α} (h : f₁ ≤ f₂) {p : α → Prop} (hp : ∀ᶠ x in f₂, p x) : ∀ᶠ x in f₁, p x

Full source

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

Monotonicity of Eventually with Respect to Filter Inclusion

Informal description

For any two filters $f_1$ and $f_2$ on a type $\alpha$, if $f_1 \leq f_2$ (i.e., $f_2 \subseteq f_1$) and the property $p$ holds eventually with respect to $f_2$, then $p$ also holds eventually with respect to $f_1$.

Filter.eventually_of_mem theorem

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

Full source

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

Eventual Truth from Filter Membership

Informal description

For any filter $f$ on a type $\alpha$, a subset $U \in f$, and a predicate $P : \alpha \to \text{Prop}$, if $P(x)$ holds for all $x \in U$, then $P(x)$ holds eventually with respect to $f$ (i.e., $\forallᶠ x \text{ in } f, P x$).

Filter.Eventually.and theorem

{p q : α → Prop} {f : Filter α} : f.Eventually p → f.Eventually q → ∀ᶠ x in f, p x ∧ q x

Full source

protected theorem Eventually.and {p q : α → Prop} {f : Filter α} :
    f.Eventually p → f.Eventually q → ∀ᶠ x in f, p x ∧ q x :=
  inter_mem

Conjunction of Eventually True Predicates is Eventually True

Informal description

For any filter $f$ on a type $\alpha$ and any two predicates $p, q : \alpha \to \text{Prop}$, if $p$ holds eventually with respect to $f$ and $q$ holds eventually with respect to $f$, then the conjunction $p(x) \land q(x)$ holds eventually with respect to $f$.

Filter.eventually_true theorem

(f : Filter α) : ∀ᶠ _ in f, True

Full source

@[simp] theorem eventually_true (f : Filter α) : ∀ᶠ _ in f, True := univ_mem

True Predicate is Eventually True for Any Filter

Informal description

For any filter $f$ on a type $\alpha$, the constantly true predicate is eventually true with respect to $f$. In other words, the set $\alpha$ (which is always in $f$) satisfies the true predicate.

Filter.Eventually.of_forall theorem

{p : α → Prop} {f : Filter α} (hp : ∀ x, p x) : ∀ᶠ x in f, p x

Full source

theorem Eventually.of_forall {p : α → Prop} {f : Filter α} (hp : ∀ x, p x) : ∀ᶠ x in f, p x :=
  univ_mem' hp

Universal Predicate Implies Eventually True

Informal description

For any filter $f$ on a type $\alpha$ and any predicate $p : \alpha \to \text{Prop}$, if $p(x)$ holds for all $x \in \alpha$, then $p$ holds eventually with respect to $f$.

Filter.eventually_false_iff_eq_bot theorem

{f : Filter α} : (∀ᶠ _ in f, False) ↔ f = ⊥

Full source

@[simp]
theorem eventually_false_iff_eq_bot {f : Filter α} : (∀ᶠ _ in f, False) ↔ f = ⊥ :=
  empty_mem_iff_bot

Characterization of Bottom Filter via Eventually False: $\forallᶠ \_ \text{ in } f, \text{False} \leftrightarrow f = \bot$

Informal description

For any filter $f$ on a type $\alpha$, the predicate $\text{False}$ holds eventually with respect to $f$ if and only if $f$ is equal to the bottom filter $\bot$ (which contains all subsets of $\alpha$). In other words, $\forallᶠ \_ \text{ in } f, \text{False} \leftrightarrow f = \bot$.

Filter.eventually_const theorem

{f : Filter α} [t : NeBot f] {p : Prop} : (∀ᶠ _ in f, p) ↔ p

Full source

@[simp]
theorem eventually_const {f : Filter α} [t : NeBot f] {p : Prop} : (∀ᶠ _ in f, p) ↔ p := by
  by_cases h : p <;> simp [h, t.ne]

Characterization of Eventually Constant Predicate for Non-trivial Filters

Informal description

For a non-trivial filter $f$ on a type $\alpha$ and a proposition $p$, the property $\forallᶠ \_ \text{ in } f, p$ holds if and only if $p$ is true.

Filter.eventually_iff_exists_mem theorem

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

Full source

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

Characterization of Eventually via Filter Membership: $\forallᶠ x \text{ in } f, p x \leftrightarrow \exists v \in f, \forall y \in v, p y$

Informal description

For any filter $f$ on a type $\alpha$ and any predicate $p : \alpha \to \text{Prop}$, the property $\forallᶠ x \text{ in } f, p x$ holds if and only if there exists a set $v \in f$ such that for all $y \in v$, $p y$ holds.

Filter.Eventually.exists_mem theorem

{p : α → Prop} {f : Filter α} (hp : ∀ᶠ x in f, p x) : ∃ v ∈ f, ∀ y ∈ v, p y

Full source

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

Existence of a Set in Filter Where Predicate Holds

Informal description

For any filter $f$ on a type $\alpha$ and any predicate $p : \alpha \to \text{Prop}$, if $p$ holds eventually in $f$ (i.e., $\forallᶠ x \text{ in } f, p x$), then there exists a set $v \in f$ such that for all $y \in v$, $p(y)$ holds.

Filter.Eventually.mp theorem

{p q : α → Prop} {f : Filter α} (hp : ∀ᶠ x in f, p x) (hq : ∀ᶠ x in f, p x → q x) : ∀ᶠ x in f, q x

Full source

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

Modus Ponens for Eventually Properties in Filters

Informal description

Let $f$ be a filter on a type $\alpha$, and let $p, q : \alpha \to \text{Prop}$ be predicates. If $p$ holds eventually in $f$ (i.e., $\forallᶠ x \text{ in } f, p x$) and the implication $p \to q$ holds eventually in $f$ (i.e., $\forallᶠ x \text{ in } f, p x \to q x$), then $q$ holds eventually in $f$ (i.e., $\forallᶠ x \text{ in } f, q x$).

Filter.Eventually.mono theorem

{p q : α → Prop} {f : Filter α} (hp : ∀ᶠ x in f, p x) (hq : ∀ x, p x → q x) : ∀ᶠ x in f, q x

Full source

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

Monotonicity of Eventually Property under Pointwise Implication

Informal description

Let $f$ be a filter on a type $\alpha$, and let $p, q : \alpha \to \text{Prop}$ be predicates. If $p$ holds eventually in $f$ (i.e., $\forallᶠ x \text{ in } f, p x$) and for every $x \in \alpha$, $p(x)$ implies $q(x)$, then $q$ holds eventually in $f$ (i.e., $\forallᶠ x \text{ in } f, q x$).

Filter.forall_eventually_of_eventually_forall theorem

{f : Filter α} {p : α → β → Prop} (h : ∀ᶠ x in f, ∀ y, p x y) : ∀ y, ∀ᶠ x in f, p x y

Full source

theorem forall_eventually_of_eventually_forall {f : Filter α} {p : α → β → Prop}
    (h : ∀ᶠ x in f, ∀ y, p x y) : ∀ y, ∀ᶠ x in f, p x y :=
  fun y => h.mono fun _ h => h y

Universal Quantifier Commutes with Eventually in Filters

Informal description

Let $f$ be a filter on a type $\alpha$ and $p : \alpha \to \beta \to \text{Prop}$ be a predicate. If for eventually all $x$ in $f$, the predicate $p(x, y)$ holds for all $y$, then for every $y$, the predicate $p(x, y)$ holds for eventually all $x$ in $f$. In other words: \[ (\forallᶠ x \text{ in } f, \forall y, p(x, y)) \implies (\forall y, \forallᶠ x \text{ in } f, p(x, y)). \]

Filter.eventually_and theorem

{p q : α → Prop} {f : Filter α} : (∀ᶠ x in f, p x ∧ q x) ↔ (∀ᶠ x in f, p x) ∧ ∀ᶠ x in f, q x

Full source

@[simp]
theorem eventually_and {p q : α → Prop} {f : Filter α} :
    (∀ᶠ x in f, p x ∧ q x) ↔ (∀ᶠ x in f, p x) ∧ ∀ᶠ x in f, q x :=
  inter_mem_iff

Filter Intersection Property: $\forallᶠ x \text{ in } f, p x \land q x \leftrightarrow (\forallᶠ x \text{ in } f, p x) \land (\forallᶠ x \text{ in } f, q x)$

Informal description

For any filter $f$ on a type $\alpha$ and any two predicates $p, q : \alpha \to \text{Prop}$, the following equivalence holds: \[ (\forallᶠ x \text{ in } f, p x \land q x) \leftrightarrow (\forallᶠ x \text{ in } f, p x) \land (\forallᶠ x \text{ in } f, q x). \]

Filter.Eventually.congr theorem

{f : Filter α} {p q : α → Prop} (h' : ∀ᶠ x in f, p x) (h : ∀ᶠ x in f, p x ↔ q x) : ∀ᶠ x in f, q x

Full source

theorem Eventually.congr {f : Filter α} {p q : α → Prop} (h' : ∀ᶠ x in f, p x)
    (h : ∀ᶠ x in f, p x ↔ q x) : ∀ᶠ x in f, q x :=
  h'.mp (h.mono fun _ hx => hx.mp)

Congruence Rule for Eventually Equivalent Properties in Filters

Informal description

Let $f$ be a filter on a type $\alpha$, and let $p, q : \alpha \to \text{Prop}$ be predicates. If $p$ holds eventually in $f$ (i.e., $\forallᶠ x \text{ in } f, p x$) and the equivalence $p(x) \leftrightarrow q(x)$ holds eventually in $f$ (i.e., $\forallᶠ x \text{ in } f, p x \leftrightarrow q x$), then $q$ holds eventually in $f$ (i.e., $\forallᶠ x \text{ in } f, q x$).

Filter.eventually_congr theorem

{f : Filter α} {p q : α → Prop} (h : ∀ᶠ x in f, p x ↔ q x) : (∀ᶠ x in f, p x) ↔ ∀ᶠ x in f, q x

Full source

theorem eventually_congr {f : Filter α} {p q : α → Prop} (h : ∀ᶠ x in f, p x ↔ q x) :
    (∀ᶠ x in f, p x) ↔ ∀ᶠ x in f, q x :=
  ⟨fun hp => hp.congr h, fun hq => hq.congr <| by simpa only [Iff.comm] using h⟩

Equivalence of Eventually Equivalent Properties in Filters

Informal description

For any filter $f$ on a type $\alpha$ and any two predicates $p, q : \alpha \to \text{Prop}$, if the equivalence $p(x) \leftrightarrow q(x)$ holds eventually in $f$ (i.e., $\forallᶠ x \text{ in } f, p x \leftrightarrow q x$), then $p$ holds eventually in $f$ if and only if $q$ holds eventually in $f$.

Filter.eventually_or_distrib_left theorem

{f : Filter α} {p : Prop} {q : α → Prop} : (∀ᶠ x in f, p ∨ q x) ↔ p ∨ ∀ᶠ x in f, q x

Full source

@[simp]
theorem eventually_or_distrib_left {f : Filter α} {p : Prop} {q : α → Prop} :
    (∀ᶠ x in f, p ∨ q x) ↔ p ∨ ∀ᶠ x in f, q x :=
  by_cases (fun h : p => by simp [h]) fun h => by simp [h]

Left Distributivity of "Eventually" over Disjunction

Informal description

For any filter $f$ on a type $\alpha$, a proposition $p$, and a predicate $q : \alpha \to \text{Prop}$, the following equivalence holds: \[ (\forallᶠ x \text{ in } f, p \lor q(x)) \leftrightarrow (p \lor (\forallᶠ x \text{ in } f, q(x))) \]

Filter.eventually_or_distrib_right theorem

{f : Filter α} {p : α → Prop} {q : Prop} : (∀ᶠ x in f, p x ∨ q) ↔ (∀ᶠ x in f, p x) ∨ q

Full source

@[simp]
theorem eventually_or_distrib_right {f : Filter α} {p : α → Prop} {q : Prop} :
    (∀ᶠ x in f, p x ∨ q) ↔ (∀ᶠ x in f, p x) ∨ q := by
  simp only [@or_comm _ q, eventually_or_distrib_left]

Distributivity of Eventually Over Disjunction (Right)

Informal description

For any filter $f$ on a type $\alpha$, any predicate $p : \alpha \to \text{Prop}$, and any proposition $q$, the following equivalence holds: \[ (\forallᶠ x \text{ in } f, p x \lor q) \leftrightarrow ((\forallᶠ x \text{ in } f, p x) \lor q). \] This means that the property "$p x$ or $q$" holds eventually with respect to $f$ if and only if either $p x$ holds eventually with respect to $f$ or $q$ holds unconditionally.

Filter.eventually_imp_distrib_left theorem

{f : Filter α} {p : Prop} {q : α → Prop} : (∀ᶠ x in f, p → q x) ↔ p → ∀ᶠ x in f, q x

Full source

theorem eventually_imp_distrib_left {f : Filter α} {p : Prop} {q : α → Prop} :
    (∀ᶠ x in f, p → q x) ↔ p → ∀ᶠ x in f, q x := by
  simp only [imp_iff_not_or, eventually_or_distrib_left]

Distributivity of Implication over Eventually with Respect to a Filter

Informal description

For any filter $f$ on a type $\alpha$, a proposition $p$, and a predicate $q : \alpha \to \text{Prop}$, the following equivalence holds: \[ (\forallᶠ x \text{ in } f, p \to q x) \leftrightarrow (p \to \forallᶠ x \text{ in } f, q x) \]

Filter.eventually_bot theorem

{p : α → Prop} : ∀ᶠ x in ⊥, p x

Full source

@[simp]
theorem eventually_bot {p : α → Prop} : ∀ᶠ x in ⊥, p x :=
  ⟨⟩

Every Property Holds Eventually in the Bottom Filter

Informal description

For any predicate $p : \alpha \to \text{Prop}$, the property $p$ holds eventually with respect to the bottom filter $\bot$ (i.e., $\forallᶠ x \text{ in } \bot, p x$ holds).

Filter.eventually_top theorem

{p : α → Prop} : (∀ᶠ x in ⊤, p x) ↔ ∀ x, p x

Full source

@[simp]
theorem eventually_top {p : α → Prop} : (∀ᶠ x in ⊤, p x) ↔ ∀ x, p x :=
  Iff.rfl

Characterization of Eventually in the Top Filter

Informal description

For any predicate $p : \alpha \to \text{Prop}$, the property $p$ holds eventually in the top filter $\top$ if and only if $p$ holds for every element $x$ in $\alpha$. In symbols: \[ (\forallᶠ x \text{ in } \top, p x) \leftrightarrow (\forall x, p x) \]

Filter.eventually_sup theorem

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

Full source

@[simp]
theorem eventually_sup {p : α → Prop} {f g : Filter α} :
    (∀ᶠ x in f ⊔ g, p x) ↔ (∀ᶠ x in f, p x) ∧ ∀ᶠ x in g, p x :=
  Iff.rfl

Eventually Property in Supremum of Two Filters

Informal description

For any predicate $p : \alpha \to \text{Prop}$ and filters $f, g$ on a type $\alpha$, the property $p$ holds eventually in the supremum filter $f \sqcup g$ if and only if $p$ holds eventually in both $f$ and $g$. In symbols: \[ \left(\forallᶠ x \text{ in } f \sqcup g, p x\right) \leftrightarrow \left(\forallᶠ x \text{ in } f, p x\right) \land \left(\forallᶠ x \text{ in } g, p x\right) \]

Filter.eventually_sSup theorem

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

Full source

@[simp]
theorem eventually_sSup {p : α → Prop} {fs : Set (Filter α)} :
    (∀ᶠ x in sSup fs, p x) ↔ ∀ f ∈ fs, ∀ᶠ x in f, p x :=
  Iff.rfl

Characterization of Eventually in Supremum of Filters

Informal description

For a predicate $p : \alpha \to \text{Prop}$ and a set of filters $\mathcal{F}$ on a type $\alpha$, the property $p$ holds eventually in the supremum filter $\bigsqcup \mathcal{F}$ if and only if for every filter $f \in \mathcal{F}$, $p$ holds eventually in $f$. In symbols: \[ \left(\forallᶠ x \text{ in } \bigsqcup \mathcal{F}, p x\right) \leftrightarrow \left(\forall f \in \mathcal{F}, \forallᶠ x \text{ in } f, p x\right) \]

Filter.eventually_iSup theorem

{p : α → Prop} {fs : ι → Filter α} : (∀ᶠ x in ⨆ b, fs b, p x) ↔ ∀ b, ∀ᶠ x in fs b, p x

Full source

@[simp]
theorem eventually_iSup {p : α → Prop} {fs : ι → Filter α} :
    (∀ᶠ x in ⨆ b, fs b, p x) ↔ ∀ b, ∀ᶠ x in fs b, p x :=
  mem_iSup

Characterization of Eventually in Indexed Supremum of Filters

Informal description

For any predicate $p : \alpha \to \text{Prop}$ and any family of filters $(f_b)_{b \in \iota}$ on a type $\alpha$, the property $p$ holds eventually in the supremum filter $\bigsqcup_{b} f_b$ if and only if for every index $b \in \iota$, $p$ holds eventually in $f_b$. In symbols: \[ \left(\forallᶠ x \text{ in } \bigsqcup_{b} f_b, p x\right) \leftrightarrow \left(\forall b, \forallᶠ x \text{ in } f_b, p x\right) \]

Filter.eventually_principal theorem

{a : Set α} {p : α → Prop} : (∀ᶠ x in 𝓟 a, p x) ↔ ∀ x ∈ a, p x

Full source

@[simp]
theorem eventually_principal {a : Set α} {p : α → Prop} : (∀ᶠ x in 𝓟 a, p x) ↔ ∀ x ∈ a, p x :=
  Iff.rfl

Characterization of Eventually in Principal Filter

Informal description

For any set $a$ in a type $\alpha$ and any predicate $p : \alpha \to \text{Prop}$, the property $p$ holds eventually in the principal filter $\mathfrak{P}(a)$ if and only if $p(x)$ holds for every $x \in a$. In other words, $\forallᶠ x \text{ in } \mathfrak{P}(a), p x \leftrightarrow \forall x \in a, p x$.

Filter.Eventually.forall_mem theorem

 {α : Type*} {f : Filter α} {s : Set α} {P : α → Prop} (hP : ∀ᶠ x in f, P x) (hf : 𝓟 s ≤ f) : ∀ x ∈ s, P x

Full source

theorem Eventually.forall_mem {α : Type*} {f : Filter α} {s : Set α} {P : α → Prop}
    (hP : ∀ᶠ x in f, P x) (hf : 𝓟 s ≤ f) : ∀ x ∈ s, P x :=
  Filter.eventually_principal.mp (hP.filter_mono hf)

Universal Property of Eventually in Principal Filter

Informal description

Let $f$ be a filter on a type $\alpha$, $s$ a subset of $\alpha$, and $P$ a predicate on $\alpha$. If $P$ holds eventually with respect to $f$ (i.e., $\forallᶠ x \text{ in } f, P x$) and the principal filter $\mathfrak{P}(s)$ is contained in $f$ (i.e., $\mathfrak{P}(s) \leq f$), then $P(x)$ holds for every $x \in s$.

Filter.eventually_inf theorem

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

Full source

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

Characterization of Eventually in Infimum Filter via Intersection

Informal description

For any filters $f$ and $g$ on a type $\alpha$ and any predicate $p : \alpha \to \mathrm{Prop}$, the following are equivalent: 1. The predicate $p$ holds eventually with respect to the infimum filter $f \sqcap g$. 2. There exist sets $s \in f$ and $t \in g$ such that $p(x)$ holds for all $x \in s \cap t$. In other words, $\forallᶠ x \text{ in } f \sqcap g, p(x) \leftrightarrow \exists s \in f, \exists t \in g, \forall x \in s \cap t, p(x)$.

Filter.eventually_inf_principal theorem

{f : Filter α} {p : α → Prop} {s : Set α} : (∀ᶠ x in f ⊓ 𝓟 s, p x) ↔ ∀ᶠ x in f, x ∈ s → p x

Full source

theorem eventually_inf_principal {f : Filter α} {p : α → Prop} {s : Set α} :
    (∀ᶠ x in f ⊓ 𝓟 s, p x) ↔ ∀ᶠ x in f, x ∈ s → p x :=
  mem_inf_principal

Equivalence of Eventual Properties in Infimum with Principal Filter

Informal description

For a filter $f$ on a type $\alpha$, a predicate $p : \alpha \to \mathrm{Prop}$, and a subset $s \subseteq \alpha$, the following are equivalent: 1. The predicate $p$ holds eventually for the infimum filter $f \sqcap \mathfrak{P}(s)$ (where $\mathfrak{P}(s)$ is the principal filter generated by $s$). 2. The implication $x \in s \to p(x)$ holds eventually for the filter $f$. In other words, $\forallᶠ x \text{ in } f \sqcap \mathfrak{P}(s), p(x)$ if and only if $\forallᶠ x \text{ in } f, x \in s \to p(x)$.

Filter.eventually_iff_all_subsets theorem

{f : Filter α} {p : α → Prop} : (∀ᶠ x in f, p x) ↔ ∀ (s : Set α), ∀ᶠ x in f, x ∈ s → p x

Full source

theorem eventually_iff_all_subsets {f : Filter α} {p : α → Prop} :
    (∀ᶠ x in f, p x) ↔ ∀ (s : Set α), ∀ᶠ x in f, x ∈ s → p x where
  mp h _ := by filter_upwards [h] with _ pa _ using pa
  mpr h := by filter_upwards [h univ] with _ pa using pa (by simp)

Characterization of Eventually via All Subsets

Informal description

For any filter $f$ on a type $\alpha$ and any predicate $p : \alpha \to \mathrm{Prop}$, the following are equivalent: 1. The property $p$ holds eventually with respect to $f$ (i.e., $\{x \mid p x\} \in f$). 2. For every subset $s \subseteq \alpha$, the implication "$x \in s$ implies $p x$" holds eventually with respect to $f$ (i.e., $\{x \mid x \in s \to p x\} \in f$ for all $s \subseteq \alpha$).

Filter.Eventually.frequently theorem

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

Full source

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

Eventual implies frequent in non-trivial filters

Informal description

For any non-trivial filter $f$ on a type $\alpha$ and any predicate $p : \alpha \to \mathrm{Prop}$, if $p$ holds eventually with respect to $f$ (i.e., $\forallᶠ x \text{ in } f, p x$), then $p$ holds frequently with respect to $f$ (i.e., $\existsᶠ x \text{ in } f, p x$).

Filter.Frequently.of_forall theorem

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

Full source

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

Universal Predicate Implies Frequently True in Non-Trivial Filters

Informal description

For any non-trivial filter $f$ on a type $\alpha$ and any predicate $p : \alpha \to \mathrm{Prop}$, if $p(x)$ holds for all $x \in \alpha$, then $p$ holds frequently with respect to $f$ (i.e., $\existsᶠ x \text{ in } f, p x$).

Filter.Frequently.mp theorem

{p q : α → Prop} {f : Filter α} (h : ∃ᶠ x in f, p x) (hpq : ∀ᶠ x in f, p x → q x) : ∃ᶠ x in f, q x

Full source

theorem Frequently.mp {p q : α → Prop} {f : Filter α} (h : ∃ᶠ x in f, p x)
    (hpq : ∀ᶠ x in f, p x → q x) : ∃ᶠ x in f, q x :=
  mt (fun hq => hq.mp <| hpq.mono fun _ => mt) h

Modus Ponens for Frequently Occurring Properties in Filters

Informal description

Let $f$ be a filter on a type $\alpha$, and let $p, q : \alpha \to \text{Prop}$ be predicates. If $p$ holds frequently in $f$ (i.e., $\existsᶠ x \text{ in } f, p x$) and the implication $p \to q$ holds eventually in $f$ (i.e., $\forallᶠ x \text{ in } f, p x \to q x$), then $q$ holds frequently in $f$ (i.e., $\existsᶠ x \text{ in } f, q x$).

Filter.frequently_congr theorem

{p q : α → Prop} {f : Filter α} (h : ∀ᶠ x in f, p x ↔ q x) : (∃ᶠ x in f, p x) ↔ ∃ᶠ x in f, q x

Full source

lemma frequently_congr {p q : α → Prop} {f : Filter α} (h : ∀ᶠ x in f, p x ↔ q x) :
    (∃ᶠ x in f, p x) ↔ ∃ᶠ x in f, q x :=
  ⟨fun h' ↦ h'.mp (h.mono fun _ ↦ Iff.mp), fun h' ↦ h'.mp (h.mono fun _ ↦ Iff.mpr)⟩

Frequently Equivalent Predicates under Filter Congruence

Informal description

For any filter $f$ on a type $\alpha$ and predicates $p, q : \alpha \to \text{Prop}$, if $p(x) \leftrightarrow q(x)$ holds eventually in $f$ (i.e., $\forallᶠ x \text{ in } f, p(x) \leftrightarrow q(x)$), then $p$ holds frequently in $f$ if and only if $q$ holds frequently in $f$ (i.e., $\existsᶠ x \text{ in } f, p(x) \leftrightarrow \existsᶠ x \text{ in } f, q(x)$).

Filter.Frequently.filter_mono theorem

{p : α → Prop} {f g : Filter α} (h : ∃ᶠ x in f, p x) (hle : f ≤ g) : ∃ᶠ x in g, p x

Full source

theorem Frequently.filter_mono {p : α → Prop} {f g : Filter α} (h : ∃ᶠ x in f, p x) (hle : f ≤ g) :
    ∃ᶠ x in g, p x :=
  mt (fun h' => h'.filter_mono hle) h

Frequently Preserved Under Filter Inclusion

Informal description

For any predicate $p : \alpha \to \text{Prop}$ and filters $f, g$ on a type $\alpha$, if $p$ holds frequently with respect to $f$ (i.e., $\existsᶠ x \text{ in } f, p x$) and $f \leq g$ (i.e., $g \subseteq f$), then $p$ also holds frequently with respect to $g$ (i.e., $\existsᶠ x \text{ in } g, p x$).

Filter.Frequently.mono theorem

{p q : α → Prop} {f : Filter α} (h : ∃ᶠ x in f, p x) (hpq : ∀ x, p x → q x) : ∃ᶠ x in f, q x

Full source

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

Frequent Property Implication in Filters

Informal description

Let $f$ be a filter on a type $\alpha$, and let $p, q : \alpha \to \text{Prop}$ be predicates. If $p$ holds frequently with respect to $f$ (i.e., $\existsᶠ x \text{ in } f, p x$) and for all $x \in \alpha$, $p(x)$ implies $q(x)$, then $q$ holds frequently with respect to $f$ (i.e., $\existsᶠ x \text{ in } f, q x$).

Filter.Frequently.and_eventually theorem

{p q : α → Prop} {f : Filter α} (hp : ∃ᶠ x in f, p x) (hq : ∀ᶠ x in f, q x) : ∃ᶠ x in f, p x ∧ q x

Full source

theorem Frequently.and_eventually {p q : α → Prop} {f : Filter α} (hp : ∃ᶠ x in f, p x)
    (hq : ∀ᶠ x in f, q x) : ∃ᶠ x in f, p x ∧ q x := by
  refine mt (fun h => hq.mp <| h.mono ?_) hp
  exact fun x hpq hq hp => hpq ⟨hp, hq⟩

Frequent and Eventually Properties Imply Frequent Conjunction

Informal description

Let $f$ be a filter on a type $\alpha$, and let $p, q : \alpha \to \text{Prop}$ be predicates. If $p$ holds frequently with respect to $f$ (i.e., $\existsᶠ x \text{ in } f, p x$) and $q$ holds eventually with respect to $f$ (i.e., $\forallᶠ x \text{ in } f, q x$), then the conjunction $p \land q$ holds frequently with respect to $f$ (i.e., $\existsᶠ x \text{ in } f, p x \land q x$).

Filter.Eventually.and_frequently theorem

{p q : α → Prop} {f : Filter α} (hp : ∀ᶠ x in f, p x) (hq : ∃ᶠ x in f, q x) : ∃ᶠ x in f, p x ∧ q x

Full source

theorem Eventually.and_frequently {p q : α → Prop} {f : Filter α} (hp : ∀ᶠ x in f, p x)
    (hq : ∃ᶠ x in f, q x) : ∃ᶠ x in f, p x ∧ q x := by
  simpa only [and_comm] using hq.and_eventually hp

Frequent Conjunction from Eventually and Frequently Occurring Properties

Informal description

Let $f$ be a filter on a type $\alpha$, and let $p, q : \alpha \to \text{Prop}$ be predicates. If $p$ holds eventually with respect to $f$ (i.e., $\forallᶠ x \text{ in } f, p x$) and $q$ holds frequently with respect to $f$ (i.e., $\existsᶠ x \text{ in } f, q x$), then the conjunction $p \land q$ holds frequently with respect to $f$ (i.e., $\existsᶠ x \text{ in } f, p x \land q x$).

Filter.Frequently.exists theorem

{p : α → Prop} {f : Filter α} (hp : ∃ᶠ x in f, p x) : ∃ x, p x

Full source

theorem Frequently.exists {p : α → Prop} {f : Filter α} (hp : ∃ᶠ x in f, p x) : ∃ x, p x := by
  by_contra H
  replace H : ∀ᶠ x in f, ¬p x := Eventually.of_forall (not_exists.1 H)
  exact hp H

Existence from Frequent Occurrence in a Filter

Informal description

For any filter $f$ on a type $\alpha$ and any predicate $p : \alpha \to \text{Prop}$, if $p$ holds frequently with respect to $f$ (i.e., $\existsᶠ x \text{ in } f, p x$), then there exists some $x \in \alpha$ for which $p(x)$ holds.

Filter.Eventually.exists theorem

{p : α → Prop} {f : Filter α} [NeBot f] (hp : ∀ᶠ x in f, p x) : ∃ x, p x

Full source

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

Existence from Eventual Occurrence in a Non-Trivial Filter

Informal description

For any non-trivial filter $f$ on a type $\alpha$ and any predicate $p : \alpha \to \mathrm{Prop}$, if $p$ holds eventually with respect to $f$ (i.e., $\forallᶠ x \text{ in } f, p x$), then there exists some $x \in \alpha$ for which $p(x)$ holds.

Filter.frequently_iff_neBot theorem

{l : Filter α} {p : α → Prop} : (∃ᶠ x in l, p x) ↔ NeBot (l ⊓ 𝓟 {x | p x})

Full source

lemma frequently_iff_neBot {l : Filter α} {p : α → Prop} :
    (∃ᶠ x in l, p x) ↔ NeBot (l ⊓ 𝓟 {x | p x}) := by
  rw [neBot_iff, Ne, inf_principal_eq_bot]; rfl

Frequent Occurrence Characterization via Non-Trivial Infimum

Informal description

For a filter $l$ on a type $\alpha$ and a predicate $p : \alpha \to \mathrm{Prop}$, the following are equivalent: 1. The property $p$ holds frequently with respect to $l$ (i.e., $\existsᶠ x \text{ in } l, p x$). 2. The infimum of $l$ and the principal filter generated by $\{x \mid p x\}$ is a non-trivial filter (i.e., $l \sqcap \mathfrak{P}(\{x \mid p x\}) \neq \bot$). In symbols: $$(\existsᶠ x \text{ in } l, p x) \leftrightarrow \text{NeBot}(l \sqcap \mathfrak{P}(\{x \mid p x\}))$$

Filter.frequently_mem_iff_neBot theorem

{l : Filter α} {s : Set α} : (∃ᶠ x in l, x ∈ s) ↔ NeBot (l ⊓ 𝓟 s)

Full source

lemma frequently_mem_iff_neBot {l : Filter α} {s : Set α} : (∃ᶠ x in l, x ∈ s) ↔ NeBot (l ⊓ 𝓟 s) :=
  frequently_iff_neBot

Frequent Membership Characterization via Non-Trivial Infimum

Informal description

For a filter $l$ on a type $\alpha$ and a subset $s \subseteq \alpha$, the following are equivalent: 1. The property $x \in s$ holds frequently with respect to $l$ (i.e., $\existsᶠ x \text{ in } l, x \in s$). 2. The infimum of $l$ and the principal filter generated by $s$ is non-trivial (i.e., $l \sqcap \mathfrak{P}(s) \neq \bot$). In symbols: $$(\existsᶠ x \text{ in } l, x \in s) \leftrightarrow \text{NeBot}(l \sqcap \mathfrak{P}(s))$$

Filter.frequently_iff_forall_eventually_exists_and theorem

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

Full source

theorem frequently_iff_forall_eventually_exists_and {p : α → Prop} {f : Filter α} :
    (∃ᶠ x in f, p x) ↔ ∀ {q : α → Prop}, (∀ᶠ x in f, q x) → ∃ x, p x ∧ q x :=
  ⟨fun hp _ hq => (hp.and_eventually hq).exists, fun H hp => by
    simpa only [and_not_self_iff, exists_false] using H hp⟩

Characterization of Frequent Occurrence via Eventual Properties

Informal description

For a filter $f$ on a type $\alpha$ and a predicate $p : \alpha \to \mathrm{Prop}$, the following are equivalent: 1. $p$ holds frequently with respect to $f$ (i.e., $\existsᶠ x \text{ in } f, p x$) 2. For every predicate $q : \alpha \to \mathrm{Prop}$ such that $q$ holds eventually with respect to $f$ (i.e., $\forallᶠ x \text{ in } f, q x$), there exists some $x \in \alpha$ for which both $p(x)$ and $q(x)$ hold. In symbols: $$(\existsᶠ x \text{ in } f, p x) \leftrightarrow \forall q, (\forallᶠ x \text{ in } f, q x) \to \exists x, p x \land q x$$

Filter.frequently_iff theorem

{f : Filter α} {P : α → Prop} : (∃ᶠ x in f, P x) ↔ ∀ {U}, U ∈ f → ∃ x ∈ U, P x

Full source

theorem frequently_iff {f : Filter α} {P : α → Prop} :
    (∃ᶠ x in f, P x) ↔ ∀ {U}, U ∈ f → ∃ x ∈ U, P x := by
  simp only [frequently_iff_forall_eventually_exists_and, @and_comm (P _)]
  rfl

Characterization of Frequent Occurrence in a Filter

Informal description

For a filter $f$ on a type $\alpha$ and a predicate $P : \alpha \to \mathrm{Prop}$, the property $P$ holds frequently with respect to $f$ (denoted $\existsᶠ x \text{ in } f, P x$) if and only if for every set $U$ in the filter $f$, there exists an element $x \in U$ such that $P x$ holds.

Filter.not_eventually theorem

{p : α → Prop} {f : Filter α} : (¬∀ᶠ x in f, p x) ↔ ∃ᶠ x in f, ¬p x

Full source

@[simp]
theorem not_eventually {p : α → Prop} {f : Filter α} : (¬∀ᶠ x in f, p x) ↔ ∃ᶠ x in f, ¬p x := by
  simp [Filter.Frequently]

Negation of Eventually is Equivalent to Frequently of Negation

Informal description

For any filter $f$ on a type $\alpha$ and any predicate $p : \alpha \to \text{Prop}$, the property $p$ does not hold eventually with respect to $f$ if and only if the negation of $p$ holds frequently with respect to $f$. In other words: $$\neg(\forallᶠ x \text{ in } f, p x) \leftrightarrow \existsᶠ x \text{ in } f, \neg p x$$

Filter.not_frequently theorem

{p : α → Prop} {f : Filter α} : (¬∃ᶠ x in f, p x) ↔ ∀ᶠ x in f, ¬p x

Full source

@[simp]
theorem not_frequently {p : α → Prop} {f : Filter α} : (¬∃ᶠ x in f, p x) ↔ ∀ᶠ x in f, ¬p x := by
  simp only [Filter.Frequently, not_not]

Negation of Frequently is Equivalent to Eventually Not

Informal description

For any filter $f$ on a type $\alpha$ and any predicate $p : \alpha \to \text{Prop}$, the following equivalence holds: $\neg (\existsᶠ x \text{ in } f, p x) \leftrightarrow \forallᶠ x \text{ in } f, \neg p x$. In other words, the property $p$ does not hold frequently with respect to $f$ if and only if the negation of $p$ holds eventually with respect to $f$.

Filter.frequently_true_iff_neBot theorem

(f : Filter α) : (∃ᶠ _ in f, True) ↔ NeBot f

Full source

@[simp]
theorem frequently_true_iff_neBot (f : Filter α) : (∃ᶠ _ in f, True) ↔ NeBot f := by
  simp [frequently_iff_neBot]

Frequently True Property Characterizes Non-Trivial Filters

Informal description

For any filter $f$ on a type $\alpha$, the property "True" holds frequently with respect to $f$ (i.e., $\existsᶠ \_ \text{ in } f, \text{True}$) if and only if $f$ is a non-trivial filter (i.e., $f \neq \bot$).

Filter.frequently_false theorem

(f : Filter α) : ¬∃ᶠ _ in f, False

Full source

@[simp]
theorem frequently_false (f : Filter α) : ¬∃ᶠ _ in f, False := by simp

No Filter Satisfies Frequently False

Informal description

For any filter $f$ on a type $\alpha$, the property "False" does not hold frequently with respect to $f$. In other words, there does not exist a set in $f$ where "False" holds for any element.

Filter.frequently_const theorem

{f : Filter α} [NeBot f] {p : Prop} : (∃ᶠ _ in f, p) ↔ p

Full source

@[simp]
theorem frequently_const {f : Filter α} [NeBot f] {p : Prop} : (∃ᶠ _ in f, p) ↔ p := by
  by_cases p <;> simp [*]

Frequently Constant Property in Non-Trivial Filter

Informal description

For a non-trivial filter $f$ on a type $\alpha$ and a proposition $p$, the property $p$ holds frequently with respect to $f$ (i.e., $\existsᶠ \_ \text{ in } f, p$) if and only if $p$ holds.

Filter.frequently_or_distrib theorem

{f : Filter α} {p q : α → Prop} : (∃ᶠ x in f, p x ∨ q x) ↔ (∃ᶠ x in f, p x) ∨ ∃ᶠ x in f, q x

Full source

@[simp]
theorem frequently_or_distrib {f : Filter α} {p q : α → Prop} :
    (∃ᶠ x in f, p x ∨ q x) ↔ (∃ᶠ x in f, p x) ∨ ∃ᶠ x in f, q x := by
  simp only [Filter.Frequently, ← not_and_or, not_or, eventually_and]

Distributivity of "Frequently" over Disjunction

Informal description

For any filter $f$ on a type $\alpha$ and any two predicates $p, q : \alpha \to \text{Prop}$, the property "frequently $p$ or $q$" holds with respect to $f$ if and only if either "frequently $p$" holds or "frequently $q$" holds with respect to $f$. In other words: \[ \existsᶠ x \text{ in } f, p x \lor q x \leftrightarrow (\existsᶠ x \text{ in } f, p x) \lor (\existsᶠ x \text{ in } f, q x). \]

Filter.frequently_or_distrib_left theorem

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

Full source

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

Distributivity of Frequently over Disjunction with a Proposition on the Left

Informal description

For a non-trivial filter $f$ on a type $\alpha$, a proposition $p$, and a predicate $q : \alpha \to \text{Prop}$, the following equivalence holds: \[ (\existsᶠ x \text{ in } f, p \lor q(x)) \leftrightarrow (p \lor \existsᶠ x \text{ in } f, q(x)). \]

Filter.frequently_or_distrib_right theorem

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

Full source

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

Distributivity of Frequently Over Disjunction with a Proposition (Right)

Informal description

For a non-trivial filter $f$ on a type $\alpha$, a predicate $p : \alpha \to \text{Prop}$, and a proposition $q$, the following equivalence holds: $\left(\existsᶠ x \text{ in } f, p(x) \lor q\right) \leftrightarrow \left(\existsᶠ x \text{ in } f, p(x)\right) \lor q$.

Filter.frequently_imp_distrib theorem

{f : Filter α} {p q : α → Prop} : (∃ᶠ x in f, p x → q x) ↔ (∀ᶠ x in f, p x) → ∃ᶠ x in f, q x

Full source

theorem frequently_imp_distrib {f : Filter α} {p q : α → Prop} :
    (∃ᶠ x in f, p x → q x) ↔ (∀ᶠ x in f, p x) → ∃ᶠ x in f, q x := by
  simp [imp_iff_not_or]

Frequently Implies Distributivity over Eventually and Frequently

Informal description

For any filter $f$ on a type $\alpha$ and predicates $p, q : \alpha \to \text{Prop}$, the following equivalence holds: \[ (\existsᶠ x \text{ in } f, p x \to q x) \leftrightarrow \big((\forallᶠ x \text{ in } f, p x) \to (\existsᶠ x \text{ in } f, q x)\big). \] This means that the property "$p x \to q x$" holds frequently in $f$ if and only if the implication "if $p x$ holds eventually in $f$, then $q x$ holds frequently in $f$" is true.

Filter.frequently_imp_distrib_left theorem

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

Full source

theorem frequently_imp_distrib_left {f : Filter α} [NeBot f] {p : Prop} {q : α → Prop} :
    (∃ᶠ x in f, p → q x) ↔ p → ∃ᶠ x in f, q x := by simp [frequently_imp_distrib]

Frequently Implies Distribution (Left) for Non-Trivial Filters

Informal description

Let $f$ be a non-trivial filter on a type $\alpha$. For any proposition $p$ and predicate $q : \alpha \to \text{Prop}$, the following equivalence holds: $$(\existsᶠ x \text{ in } f, p \to q(x)) \leftrightarrow (p \to \existsᶠ x \text{ in } f, q(x))$$ This means that "$p$ implies $q(x)$" holds frequently in $f$ if and only if $p$ implies that $q(x)$ holds frequently in $f$.

Filter.frequently_imp_distrib_right theorem

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

Full source

theorem frequently_imp_distrib_right {f : Filter α} [NeBot f] {p : α → Prop} {q : Prop} :
    (∃ᶠ x in f, p x → q) ↔ (∀ᶠ x in f, p x) → q := by
  simp only [frequently_imp_distrib, frequently_const]

Frequently Implies Distribution Right: $(\existsᶠ x, p x \to q) \leftrightarrow ((\forallᶠ x, p x) \to q)$

Informal description

For a non-trivial filter $f$ on a type $\alpha$, a predicate $p : \alpha \to \text{Prop}$, and a proposition $q$, the following equivalence holds: $$(\existsᶠ x \text{ in } f, p x \to q) \leftrightarrow ((\forallᶠ x \text{ in } f, p x) \to q).$$ This means that the statement "$p x \to q$ holds frequently in $f$" is equivalent to "if $p x$ holds eventually in $f$, then $q$ holds".

Filter.eventually_imp_distrib_right theorem

{f : Filter α} {p : α → Prop} {q : Prop} : (∀ᶠ x in f, p x → q) ↔ (∃ᶠ x in f, p x) → q

Full source

theorem eventually_imp_distrib_right {f : Filter α} {p : α → Prop} {q : Prop} :
    (∀ᶠ x in f, p x → q) ↔ (∃ᶠ x in f, p x) → q := by
  simp only [imp_iff_not_or, eventually_or_distrib_right, not_frequently]

Equivalence between Universal and Existential Eventual Implications in Filters

Informal description

For any filter $f$ on a type $\alpha$, a predicate $p : \alpha \to \text{Prop}$, and a proposition $q$, the following equivalence holds: \[ (\forallᶠ x \text{ in } f, p x \to q) \leftrightarrow ((\existsᶠ x \text{ in } f, p x) \to q) \] Here, $\forallᶠ x \text{ in } f, \phi x$ means "$\phi$ holds eventually in $f$" (i.e., $\{x \mid \phi x\} \in f$), and $\existsᶠ x \text{ in } f, \phi x$ means "$\phi$ holds frequently in $f$" (i.e., $\{x \mid \neg \phi x\} \notin f$).

Filter.frequently_and_distrib_left theorem

{f : Filter α} {p : Prop} {q : α → Prop} : (∃ᶠ x in f, p ∧ q x) ↔ p ∧ ∃ᶠ x in f, q x

Full source

@[simp]
theorem frequently_and_distrib_left {f : Filter α} {p : Prop} {q : α → Prop} :
    (∃ᶠ x in f, p ∧ q x) ↔ p ∧ ∃ᶠ x in f, q x := by
  simp only [Filter.Frequently, not_and, eventually_imp_distrib_left, Classical.not_imp]

Distributivity of "Frequently" over Conjunction (Left)

Informal description

For any filter $f$ on a type $\alpha$, a proposition $p$, and a predicate $q : \alpha \to \text{Prop}$, the following equivalence holds: $$(\existsᶠ x \text{ in } f, p \land q(x)) \leftrightarrow (p \land \existsᶠ x \text{ in } f, q(x))$$ This means that the property "$p$ and $q(x)$" holds frequently with respect to $f$ if and only if $p$ holds and $q(x)$ holds frequently with respect to $f$.

Filter.frequently_and_distrib_right theorem

{f : Filter α} {p : α → Prop} {q : Prop} : (∃ᶠ x in f, p x ∧ q) ↔ (∃ᶠ x in f, p x) ∧ q

Full source

@[simp]
theorem frequently_and_distrib_right {f : Filter α} {p : α → Prop} {q : Prop} :
    (∃ᶠ x in f, p x ∧ q) ↔ (∃ᶠ x in f, p x) ∧ q := by
  simp only [@and_comm _ q, frequently_and_distrib_left]

Distributivity of "Frequently" over Conjunction (Right)

Informal description

For any filter $f$ on a type $\alpha$, a predicate $p : \alpha \to \text{Prop}$, and a proposition $q$, the following equivalence holds: $$(\existsᶠ x \text{ in } f, p(x) \land q) \leftrightarrow ((\existsᶠ x \text{ in } f, p(x)) \land q)$$ This means that the property "$p(x)$ and $q$" holds frequently with respect to $f$ if and only if $p(x)$ holds frequently with respect to $f$ and $q$ holds.

Filter.frequently_bot theorem

{p : α → Prop} : ¬∃ᶠ x in ⊥, p x

Full source

@[simp]
theorem frequently_bot {p : α → Prop} : ¬∃ᶠ x in ⊥, p x := by simp

No Property Holds Frequently in the Bottom Filter

Informal description

For any predicate $p : \alpha \to \mathrm{Prop}$, the property $p$ does not hold frequently with respect to the bottom filter $\bot$ on $\alpha$. In other words, there does not exist a set in the bottom filter $\bot$ where $p$ holds for some element in that set.

Filter.frequently_top theorem

{p : α → Prop} : (∃ᶠ x in ⊤, p x) ↔ ∃ x, p x

Full source

@[simp]
theorem frequently_top {p : α → Prop} : (∃ᶠ x in ⊤, p x) ↔ ∃ x, p x := by simp [Filter.Frequently]

Frequently in Top Filter is Equivalent to Existence

Informal description

For any predicate $p : \alpha \to \text{Prop}$, the property $p$ holds frequently in the top filter $\top$ (the filter containing all subsets of $\alpha$) if and only if there exists some $x \in \alpha$ for which $p(x)$ holds.

Filter.frequently_principal theorem

{a : Set α} {p : α → Prop} : (∃ᶠ x in 𝓟 a, p x) ↔ ∃ x ∈ a, p x

Full source

@[simp]
theorem frequently_principal {a : Set α} {p : α → Prop} : (∃ᶠ x in 𝓟 a, p x) ↔ ∃ x ∈ a, p x := by
  simp [Filter.Frequently, not_forall]

Frequently in Principal Filter is Equivalent to Existence in Set

Informal description

For any set $a$ in a type $\alpha$ and any predicate $p : \alpha \to \mathrm{Prop}$, the property $p$ holds frequently in the principal filter generated by $a$ if and only if there exists an element $x \in a$ such that $p(x)$ holds. In other words, $\existsᶠ x \text{ in } \mathfrak{P}(a), p x \leftrightarrow \exists x \in a, p x$, where $\mathfrak{P}(a)$ denotes the principal filter generated by $a$.

Filter.frequently_inf_principal theorem

{f : Filter α} {s : Set α} {p : α → Prop} : (∃ᶠ x in f ⊓ 𝓟 s, p x) ↔ ∃ᶠ x in f, x ∈ s ∧ p x

Full source

theorem frequently_inf_principal {f : Filter α} {s : Set α} {p : α → Prop} :
    (∃ᶠ x in f ⊓ 𝓟 s, p x) ↔ ∃ᶠ x in f, x ∈ s ∧ p x := by
  simp only [Filter.Frequently, eventually_inf_principal, not_and]

Frequently in Infimum with Principal Filter is Equivalent to Frequently in Filter Restricted to Set

Informal description

For a filter $f$ on a type $\alpha$, a set $s \subseteq \alpha$, and a predicate $p : \alpha \to \text{Prop}$, the following are equivalent: 1. The property $p$ holds frequently in the infimum of $f$ and the principal filter generated by $s$ (i.e., $\existsᶠ x \text{ in } f \sqcap \mathfrak{P}(s), p x$). 2. The property $p$ holds frequently in $f$ for elements that are in $s$ (i.e., $\existsᶠ x \text{ in } f, x \in s \land p x$).

Filter.frequently_sup theorem

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

Full source

theorem frequently_sup {p : α → Prop} {f g : Filter α} :
    (∃ᶠ x in f ⊔ g, p x) ↔ (∃ᶠ x in f, p x) ∨ ∃ᶠ x in g, p x := by
  simp only [Filter.Frequently, eventually_sup, not_and_or]

Frequently Property in Supremum of Two Filters

Informal description

For a predicate $p : \alpha \to \text{Prop}$ and filters $f$ and $g$ on $\alpha$, the property $p$ holds frequently in the supremum filter $f \sqcup g$ if and only if $p$ holds frequently in $f$ or $p$ holds frequently in $g$. In notation: $$ \left( \existsᶠ x \text{ in } f \sqcup g, p x \right) \leftrightarrow \left( \existsᶠ x \text{ in } f, p x \right) \lor \left( \existsᶠ x \text{ in } g, p x \right) $$

Filter.frequently_sSup theorem

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

Full source

@[simp]
theorem frequently_sSup {p : α → Prop} {fs : Set (Filter α)} :
    (∃ᶠ x in sSup fs, p x) ↔ ∃ f ∈ fs, ∃ᶠ x in f, p x := by
  simp only [Filter.Frequently, not_forall, eventually_sSup, exists_prop]

Frequently Property in Supremum of Filters is Equivalent to Frequently in Some Filter

Informal description

For a predicate $p : \alpha \to \text{Prop}$ and a set of filters $\mathcal{F}$ on $\alpha$, the following are equivalent: 1. The property $p$ holds frequently in the supremum of $\mathcal{F}$ (i.e., $\existsᶠ x \text{ in } \bigsqcup \mathcal{F}, p x$). 2. There exists a filter $f \in \mathcal{F}$ such that $p$ holds frequently in $f$ (i.e., $\exists f \in \mathcal{F}, \existsᶠ x \text{ in } f, p x$).

Filter.frequently_iSup theorem

{p : α → Prop} {fs : β → Filter α} : (∃ᶠ x in ⨆ b, fs b, p x) ↔ ∃ b, ∃ᶠ x in fs b, p x

Full source

@[simp]
theorem frequently_iSup {p : α → Prop} {fs : β → Filter α} :
    (∃ᶠ x in ⨆ b, fs b, p x) ↔ ∃ b, ∃ᶠ x in fs b, p x := by
  simp only [Filter.Frequently, eventually_iSup, not_forall]

Frequently Property in Supremum of Filters

Informal description

For a predicate $p : \alpha \to \text{Prop}$ and a family of filters $(f_b)_{b \in \beta}$ on $\alpha$, the property $p$ holds frequently in the supremum filter $\bigsqcup_{b} f_b$ if and only if there exists some index $b$ such that $p$ holds frequently in $f_b$. In notation: $$ \left( \existsᶠ x \text{ in } \bigsqcup_{b} f_b, p x \right) \leftrightarrow \exists b, \existsᶠ x \text{ in } f_b, p x $$

Filter.Eventually.choice theorem

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

Full source

theorem Eventually.choice {r : α → β → Prop} {l : Filter α} [l.NeBot] (h : ∀ᶠ x in l, ∃ y, r x y) :
    ∃ f : α → β, ∀ᶠ x in l, r x (f x) := by
  haveI : Nonempty β := let ⟨_, hx⟩ := h.exists; hx.nonempty
  choose! f hf using fun x (hx : ∃ y, r x y) => hx
  exact ⟨f, h.mono hf⟩

Existence of Choice Function for Eventual Existence in Non-Trivial Filter

Informal description

Let $\alpha$ and $\beta$ be types, $r : \alpha \to \beta \to \text{Prop}$ a relation, and $l$ a non-trivial filter on $\alpha$. If for all $x$ in some set belonging to $l$, there exists $y \in \beta$ such that $r(x,y)$ holds, then there exists a function $f : \alpha \to \beta$ such that for all $x$ in some set belonging to $l$, the relation $r(x, f(x))$ holds. In notation: $$ \left( \forallᶠ x \text{ in } l, \exists y, r(x,y) \right) \implies \exists f : \alpha \to \beta, \forallᶠ x \text{ in } l, r(x, f(x)) $$

Filter.skolem theorem

 {ι : Type*} {α : ι → Type*} [∀ i, Nonempty (α i)] {P : ∀ i : ι, α i → Prop} {F : Filter ι} :
  (∀ᶠ i in F, ∃ b, P i b) ↔ ∃ b : (Π i, α i), ∀ᶠ i in F, P i (b i)

Full source

lemma skolem {ι : Type*} {α : ι → Type*} [∀ i, Nonempty (α i)]
    {P : ∀ i : ι, α i → Prop} {F : Filter ι} :
    (∀ᶠ i in F, ∃ b, P i b) ↔ ∃ b : (Π i, α i), ∀ᶠ i in F, P i (b i) := by
  classical
  refine ⟨fun H ↦ ?_, fun ⟨b, hb⟩ ↦ hb.mp (.of_forall fun x a ↦ ⟨_, a⟩)⟩
  refine ⟨fun i ↦ if h : ∃ b, P i b then h.choose else Nonempty.some inferInstance, ?_⟩
  filter_upwards [H] with i hi
  exact dif_pos hi ▸ hi.choose_spec

Skolem Property for Filters on Nonempty Types

Informal description

Let $\iota$ be a type, and for each $i \in \iota$, let $\alpha_i$ be a nonempty type. Given a predicate $P : \prod_{i \in \iota} (\alpha_i \to \text{Prop})$ and a filter $F$ on $\iota$, the following are equivalent: 1. For all $i$ in some set belonging to $F$, there exists $b \in \alpha_i$ such that $P_i(b)$ holds. 2. There exists a function $b : \prod_{i \in \iota} \alpha_i$ such that for all $i$ in some set belonging to $F$, $P_i(b(i))$ holds. In notation: $$ \left( \forallᶠ i \text{ in } F, \exists b, P_i b \right) \leftrightarrow \exists b : \prod_{i} \alpha_i, \forallᶠ i \text{ in } F, P_i (b i) $$

Filter.EventuallyEq.eventually theorem

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

Full source

theorem EventuallyEq.eventually (h : f =ᶠ[l] g) : ∀ᶠ x in l, f x = g x := h

Eventual equality implies pointwise equality on a filter set

Informal description

If two functions $f$ and $g$ are eventually equal with respect to a filter $l$ (i.e., $f =ᶠ[l] g$), then for all $x$ in some set belonging to $l$, we have $f(x) = g(x)$.

Filter.eventuallyEq_top theorem

: f =ᶠ[⊤] g ↔ f = g

Full source

@[simp] lemma eventuallyEq_top : f =ᶠ[⊤] gf =ᶠ[⊤] g ↔ f = g := by simp [EventuallyEq, funext_iff]

Eventual equality under top filter is equivalent to global equality

Informal description

Two functions $f$ and $g$ from $\alpha$ to $\beta$ are eventually equal with respect to the top filter (the filter containing all subsets of $\alpha$) if and only if $f$ and $g$ are equal as functions, i.e., $f(x) = g(x)$ for all $x \in \alpha$.

Filter.EventuallyEq.rw theorem

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

Full source

theorem EventuallyEq.rw {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) :=
  hf.congr <| h.mono fun _ hx => hx ▸ Iff.rfl

Substitution of Eventually Equal Functions in Predicates

Informal description

Let $l$ be a filter on a type $\alpha$, and let $f, g : \alpha \to \beta$ be functions. If $f$ and $g$ are eventually equal with respect to $l$ (i.e., $f(x) = g(x)$ for all $x$ in some set belonging to $l$), and if for some predicate $p : \alpha \to \beta \to \text{Prop}$ we have $p(x, f(x))$ holds eventually in $l$, then $p(x, g(x))$ also holds eventually in $l$.

Filter.eventuallyEq_set theorem

{s t : Set α} {l : Filter α} : s =ᶠ[l] t ↔ ∀ᶠ x in l, x ∈ s ↔ x ∈ t

Full source

theorem eventuallyEq_set {s t : Set α} {l : Filter α} : s =ᶠ[l] ts =ᶠ[l] t ↔ ∀ᶠ x in l, x ∈ s ↔ x ∈ t :=
  eventually_congr <| Eventually.of_forall fun _ ↦ eq_iff_iff

Characterization of Eventually Equal Sets via Membership Equivalence

Informal description

For any two sets $s$ and $t$ in a type $\alpha$ and any filter $l$ on $\alpha$, the sets $s$ and $t$ are eventually equal with respect to $l$ if and only if the membership conditions $x \in s$ and $x \in t$ are eventually equivalent in $l$ (i.e., $\{x \mid x \in s \leftrightarrow x \in t\} \in l$).

Filter.eventuallyEq_univ theorem

{s : Set α} {l : Filter α} : s =ᶠ[l] univ ↔ s ∈ l

Full source

@[simp]
theorem eventuallyEq_univ {s : Set α} {l : Filter α} : s =ᶠ[l] univs =ᶠ[l] univ ↔ s ∈ l := by
  simp [eventuallyEq_set]

Equivalence of Eventually Equal to Universal Set and Filter Membership

Informal description

For any set $s$ in a type $\alpha$ and any filter $l$ on $\alpha$, the set $s$ is eventually equal to the universal set with respect to $l$ if and only if $s$ belongs to the filter $l$. In other words, $s =ᶠ[l] \text{univ} \leftrightarrow s \in l$.

Filter.EventuallyEq.exists_mem theorem

{l : Filter α} {f g : α → β} (h : f =ᶠ[l] g) : ∃ s ∈ l, EqOn f g s

Full source

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

Existence of a Filter Set Where Functions Agree

Informal description

For any filter $l$ on a type $\alpha$ and any functions $f, g : \alpha \to \beta$, if $f$ and $g$ are eventually equal with respect to $l$ (i.e., $\{x \mid f(x) = g(x)\} \in l$), then there exists a set $s \in l$ such that $f$ and $g$ agree on $s$ (i.e., $f(x) = g(x)$ for all $x \in s$).

Filter.eventuallyEq_of_mem theorem

{l : Filter α} {f g : α → β} {s : Set α} (hs : s ∈ l) (h : EqOn f g s) : f =ᶠ[l] g

Full source

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

Agreement on a Filter Set Implies Eventual Equality

Informal description

Let $l$ be a filter on a type $\alpha$, and let $f, g : \alpha \to \beta$ be functions. If there exists a set $s \in l$ such that $f$ and $g$ agree on $s$ (i.e., $f(x) = g(x)$ for all $x \in s$), then $f$ and $g$ are eventually equal with respect to $l$ (i.e., $\{x \mid f(x) = g(x)\} \in l$).

Filter.eventuallyEq_iff_exists_mem theorem

{l : Filter α} {f g : α → β} : f =ᶠ[l] g ↔ ∃ s ∈ l, EqOn f g s

Full source

theorem eventuallyEq_iff_exists_mem {l : Filter α} {f g : α → β} :
    f =ᶠ[l] gf =ᶠ[l] g ↔ ∃ s ∈ l, EqOn f g s :=
  eventually_iff_exists_mem

Characterization of Eventually Equal Functions via Filter Membership: $f =ᶠ[l] g \leftrightarrow \exists s \in l, \forall x \in s, f(x) = g(x)$

Informal description

For a filter $l$ on a type $\alpha$ and functions $f, g : \alpha \to \beta$, the functions are eventually equal with respect to $l$ (i.e., $f =ᶠ[l] g$) if and only if there exists a set $s \in l$ such that $f$ and $g$ agree on $s$ (i.e., $f(x) = g(x)$ for all $x \in s$).

Filter.EventuallyEq.filter_mono theorem

{l l' : Filter α} {f g : α → β} (h₁ : f =ᶠ[l] g) (h₂ : l' ≤ l) : f =ᶠ[l'] g

Full source

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

Monotonicity of Eventually Equal Functions with Respect to Filter Order

Informal description

Let $l$ and $l'$ be filters on a type $\alpha$, and let $f, g : \alpha \to \beta$ be functions. If $f$ and $g$ are eventually equal with respect to $l$ (i.e., $\{x \mid f(x) = g(x)\} \in l$) and $l' \leq l$ in the partial order of filters, then $f$ and $g$ are also eventually equal with respect to $l'$.

Filter.EventuallyEq.refl theorem

(l : Filter α) (f : α → β) : f =ᶠ[l] f

Full source

@[refl, simp]
theorem EventuallyEq.refl (l : Filter α) (f : α → β) : f =ᶠ[l] f :=
  Eventually.of_forall fun _ => rfl

Reflexivity of Eventually Equal Relation

Informal description

For any filter $l$ on a type $\alpha$ and any function $f : \alpha \to \beta$, the function $f$ is eventually equal to itself with respect to $l$. In other words, the set $\{x \in \alpha \mid f(x) = f(x)\}$ belongs to the filter $l$.

Filter.EventuallyEq.rfl theorem

{l : Filter α} {f : α → β} : f =ᶠ[l] f

Full source

protected theorem EventuallyEq.rfl {l : Filter α} {f : α → β} : f =ᶠ[l] f :=
  EventuallyEq.refl l f

Reflexivity of Eventually Equal Relation

Informal description

For any filter $l$ on a type $\alpha$ and any function $f : \alpha \to \beta$, the function $f$ is eventually equal to itself with respect to $l$. That is, the set $\{x \in \alpha \mid f(x) = f(x)\}$ belongs to the filter $l$.

Filter.EventuallyEq.of_eq theorem

{l : Filter α} {f g : α → β} (h : f = g) : f =ᶠ[l] g

Full source

theorem EventuallyEq.of_eq {l : Filter α} {f g : α → β} (h : f = g) : f =ᶠ[l] g := h ▸ .rfl

Pointwise equality implies eventual equality with respect to a filter

Informal description

For any filter $l$ on a type $\alpha$ and any functions $f, g : \alpha \to \beta$, if $f = g$ (pointwise equality), then $f$ is eventually equal to $g$ with respect to $l$. That is, the set $\{x \in \alpha \mid f(x) = g(x)\}$ belongs to the filter $l$.

Filter.EventuallyEq.symm theorem

{f g : α → β} {l : Filter α} (H : f =ᶠ[l] g) : g =ᶠ[l] f

Full source

@[symm]
theorem EventuallyEq.symm {f g : α → β} {l : Filter α} (H : f =ᶠ[l] g) : g =ᶠ[l] f :=
  H.mono fun _ => Eq.symm

Symmetry of Eventually Equal Functions

Informal description

For any two functions $f, g : \alpha \to \beta$ and a filter $l$ on $\alpha$, if $f$ is eventually equal to $g$ with respect to $l$ (i.e., $f =ᶠ[l] g$), then $g$ is eventually equal to $f$ with respect to $l$ (i.e., $g =ᶠ[l] f$).

Filter.eventuallyEq_comm theorem

{f g : α → β} {l : Filter α} : f =ᶠ[l] g ↔ g =ᶠ[l] f

Full source

lemma eventuallyEq_comm {f g : α → β} {l : Filter α} : f =ᶠ[l] gf =ᶠ[l] g ↔ g =ᶠ[l] f := ⟨.symm, .symm⟩

Commutativity of Eventually Equal Relation

Informal description

For any two functions $f, g : \alpha \to \beta$ and a filter $l$ on $\alpha$, the statements $f$ is eventually equal to $g$ with respect to $l$ and $g$ is eventually equal to $f$ with respect to $l$ are equivalent. In other words, $f =ᶠ[l] g$ if and only if $g =ᶠ[l] f$.

Filter.EventuallyEq.trans theorem

{l : Filter α} {f g h : α → β} (H₁ : f =ᶠ[l] g) (H₂ : g =ᶠ[l] h) : f =ᶠ[l] h

Full source

@[trans]
theorem EventuallyEq.trans {l : Filter α} {f g h : α → β} (H₁ : f =ᶠ[l] g) (H₂ : g =ᶠ[l] h) :
    f =ᶠ[l] h :=
  H₂.rw (fun x y => f x = y) H₁

Transitivity of Eventually Equal Functions

Informal description

Let $l$ be a filter on a type $\alpha$, and let $f, g, h : \alpha \to \beta$ be functions. If $f$ is eventually equal to $g$ with respect to $l$ (i.e., $f(x) = g(x)$ for all $x$ in some set belonging to $l$), and $g$ is eventually equal to $h$ with respect to $l$, then $f$ is eventually equal to $h$ with respect to $l$.

Filter.EventuallyEq.congr_left theorem

{l : Filter α} {f g h : α → β} (H : f =ᶠ[l] g) : f =ᶠ[l] h ↔ g =ᶠ[l] h

Full source

theorem EventuallyEq.congr_left {l : Filter α} {f g h : α → β} (H : f =ᶠ[l] g) :
    f =ᶠ[l] hf =ᶠ[l] h ↔ g =ᶠ[l] h :=
  ⟨H.symm.trans, H.trans⟩

Left Congruence Property of Eventually Equal Functions

Informal description

Let $l$ be a filter on a type $\alpha$, and let $f, g, h : \alpha \to \beta$ be functions. If $f$ is eventually equal to $g$ with respect to $l$ (i.e., $f =ᶠ[l] g$), then the statements $f =ᶠ[l] h$ and $g =ᶠ[l] h$ are equivalent.

Filter.EventuallyEq.congr_right theorem

{l : Filter α} {f g h : α → β} (H : g =ᶠ[l] h) : f =ᶠ[l] g ↔ f =ᶠ[l] h

Full source

theorem EventuallyEq.congr_right {l : Filter α} {f g h : α → β} (H : g =ᶠ[l] h) :
    f =ᶠ[l] gf =ᶠ[l] g ↔ f =ᶠ[l] h :=
  ⟨(·.trans H), (·.trans H.symm)⟩

Right Congruence Property of Eventually Equal Functions

Informal description

Let $l$ be a filter on a type $\alpha$, and let $f, g, h : \alpha \to \beta$ be functions. If $g$ is eventually equal to $h$ with respect to $l$ (i.e., $g =ᶠ[l] h$), then for any function $f$, the statements $f =ᶠ[l] g$ and $f =ᶠ[l] h$ are equivalent.

Filter.instTransForallEventuallyEq instance

{l : Filter α} : Trans ((· =ᶠ[l] ·) : (α → β) → (α → β) → Prop) (· =ᶠ[l] ·) (· =ᶠ[l] ·)

Full source

instance {l : Filter α} :
    Trans ((· =ᶠ[l] ·) : (α → β) → (α → β) → Prop) (· =ᶠ[l] ·) (· =ᶠ[l] ·) where
  trans := EventuallyEq.trans

Transitivity of Eventual Equality under a Filter

Informal description

For any filter $l$ on a type $\alpha$, the relation of eventual equality $=ᶠ[l]$ is transitive on functions from $\alpha$ to $\beta$. That is, if $f =ᶠ[l] g$ and $g =ᶠ[l] h$, then $f =ᶠ[l] h$.

Filter.EventuallyEq.prodMk theorem

 {l} {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)

Full source

theorem EventuallyEq.prodMk {l} {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) :=
  hf.mp <|
    hg.mono <| by
      intros
      simp only [*]

Pairwise Eventually Equal Functions under Filter

Informal description

Let $l$ be a filter on a type $\alpha$, and let $f, f' : \alpha \to \beta$ and $g, g' : \alpha \to \gamma$ be functions. If $f$ and $f'$ are eventually equal with respect to $l$ (i.e., $f =ᶠ[l] f'$) and $g$ and $g'$ are eventually equal with respect to $l$ (i.e., $g =ᶠ[l] g'$), then the functions $x \mapsto (f(x), g(x))$ and $x \mapsto (f'(x), g'(x))$ are also eventually equal with respect to $l$.

Filter.EventuallyEq.fun_comp theorem

{f g : α → β} {l : Filter α} (H : f =ᶠ[l] g) (h : β → γ) : h ∘ f =ᶠ[l] h ∘ g

Full source

theorem EventuallyEq.fun_comp {f g : α → β} {l : Filter α} (H : f =ᶠ[l] g) (h : β → γ) :
    h ∘ fh ∘ f =ᶠ[l] h ∘ g :=
  H.mono fun _ hx => congr_arg h hx

Composition Preserves Eventually Equal Functions

Informal description

Let $f, g : \alpha \to \beta$ be functions and $l$ be a filter on $\alpha$. If $f$ and $g$ are eventually equal with respect to $l$ (i.e., $f =ᶠ[l] g$), then for any function $h : \beta \to \gamma$, the compositions $h \circ f$ and $h \circ g$ are also eventually equal with respect to $l$ (i.e., $h \circ f =ᶠ[l] h \circ g$).

Filter.EventuallyEq.comp₂ theorem

 {δ} {f f' : α → β} {g g' : α → γ} {l} (Hf : f =ᶠ[l] f') (h : β → γ → δ) (Hg : g =ᶠ[l] g') :
  (fun x => h (f x) (g x)) =ᶠ[l] fun x => h (f' x) (g' x)

Full source

theorem EventuallyEq.comp₂ {δ} {f f' : α → β} {g g' : α → γ} {l} (Hf : f =ᶠ[l] f') (h : β → γ → δ)
    (Hg : g =ᶠ[l] g') : (fun x => h (f x) (g x)) =ᶠ[l] fun x => h (f' x) (g' x) :=
  (Hf.prodMk Hg).fun_comp (uncurry h)

Binary Operation Preserves Eventually Equal Functions under Filter

Informal description

Let $l$ be a filter on a type $\alpha$, and let $f, f' : \alpha \to \beta$ and $g, g' : \alpha \to \gamma$ be functions. If $f$ and $f'$ are eventually equal with respect to $l$ (i.e., $f =ᶠ[l] f'$) and $g$ and $g'$ are eventually equal with respect to $l$ (i.e., $g =ᶠ[l] g'$), then for any binary function $h : \beta \to \gamma \to \delta$, the functions $x \mapsto h(f(x), g(x))$ and $x \mapsto h(f'(x), g'(x))$ are also eventually equal with respect to $l$.

Filter.EventuallyEq.mul theorem

 [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

Full source

@[to_additive]
theorem EventuallyEq.mul [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 :=
  h.comp₂ (· * ·) h'

Pointwise Multiplication Preserves Eventually Equal Functions

Informal description

Let $\beta$ be a type with a multiplication operation, and let $f, f', g, g' : \alpha \to \beta$ be functions. Given a filter $l$ on $\alpha$, if $f$ and $g$ are eventually equal with respect to $l$ (i.e., $f(x) = g(x)$ for all $x$ in some set in $l$), and $f'$ and $g'$ are eventually equal with respect to $l$, then the pointwise products $x \mapsto f(x) * f'(x)$ and $x \mapsto g(x) * g'(x)$ are also eventually equal with respect to $l$.

Filter.EventuallyEq.pow_const theorem

 {γ} [Pow β γ] {f g : α → β} {l : Filter α} (h : f =ᶠ[l] g) (c : γ) : (fun x => f x ^ c) =ᶠ[l] fun x => g x ^ c

Full source

@[to_additive const_smul]
theorem EventuallyEq.pow_const {γ} [Pow β γ] {f g : α → β} {l : Filter α} (h : f =ᶠ[l] g) (c : γ) :
    (fun x => f x ^ c) =ᶠ[l] fun x => g x ^ c :=
  h.fun_comp (· ^ c)

Preservation of Eventually Equal Functions under Constant Power Operation

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be types, with a power operation $\cdot^\cdot : \beta \times \gamma \to \beta$ defined on $\beta$. Let $f, g : \alpha \to \beta$ be functions and $l$ be a filter on $\alpha$. If $f$ and $g$ are eventually equal with respect to $l$ (i.e., $f(x) = g(x)$ for all $x$ in some set belonging to $l$), then for any constant $c \in \gamma$, the functions $x \mapsto f(x)^c$ and $x \mapsto g(x)^c$ are also eventually equal with respect to $l$.

Filter.EventuallyEq.inv theorem

[Inv β] {f g : α → β} {l : Filter α} (h : f =ᶠ[l] g) : (fun x => (f x)⁻¹) =ᶠ[l] fun x => (g x)⁻¹

Full source

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

Pointwise Inversion Preserves Eventually Equal Functions

Informal description

Let $\beta$ be a type with an inversion operation $(\cdot)^{-1}$, and let $f, g : \alpha \to \beta$ be functions. If $f$ and $g$ are eventually equal with respect to a filter $l$ on $\alpha$ (i.e., $f(x) = g(x)$ for all $x$ in some set belonging to $l$), then their pointwise inverses $(f(\cdot))^{-1}$ and $(g(\cdot))^{-1}$ are also eventually equal with respect to $l$.

Filter.EventuallyEq.div theorem

 [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

Full source

@[to_additive]
theorem EventuallyEq.div [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 :=
  h.comp₂ (· / ·) h'

Pointwise Division Preserves Eventually Equal Functions

Informal description

Let $\beta$ be a type with a division operation $(\cdot)/(\cdot) : \beta \times \beta \to \beta$, and let $f, g, f', g' : \alpha \to \beta$ be functions. If $f$ and $g$ are eventually equal with respect to a filter $l$ on $\alpha$ (i.e., $f(x) = g(x)$ for all $x$ in some set belonging to $l$), and $f'$ and $g'$ are also eventually equal with respect to $l$, then the pointwise quotients $x \mapsto f(x)/f'(x)$ and $x \mapsto g(x)/g'(x)$ are eventually equal with respect to $l$.

Filter.EventuallyEq.smul theorem

 {𝕜} [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

Full source

@[to_additive]
theorem EventuallyEq.smul {𝕜} [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 :=
  hf.comp₂ (· • ·) hg

Scalar Multiplication Preserves Eventually Equal Functions under Filter

Informal description

Let $\mathbb{K}$ be a type equipped with a scalar multiplication operation $\cdot \colon \mathbb{K} \times \beta \to \beta$, and let $l$ be a filter on a type $\alpha$. Suppose $f, f' \colon \alpha \to \mathbb{K}$ and $g, g' \colon \alpha \to \beta$ are functions such that: - $f$ and $f'$ are eventually equal with respect to $l$ (i.e., $f =ᶠ[l] f'$), - $g$ and $g'$ are eventually equal with respect to $l$ (i.e., $g =ᶠ[l] g'$). Then the functions $x \mapsto f(x) \cdot g(x)$ and $x \mapsto f'(x) \cdot g'(x)$ are also eventually equal with respect to $l$.

Filter.EventuallyEq.sup theorem

 [Max β] {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

Full source

theorem EventuallyEq.sup [Max β] {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 :=
  hf.comp₂ (· ⊔ ·) hg

Supremum Preserves Eventually Equal Functions under Filter

Informal description

Let $l$ be a filter on a type $\alpha$, and let $f, f', g, g' : \alpha \to \beta$ be functions where $\beta$ is equipped with a maximum operation $\sqcup$. If $f$ and $f'$ are eventually equal with respect to $l$ (i.e., $f =_l f'$) and $g$ and $g'$ are eventually equal with respect to $l$ (i.e., $g =_l g'$), then the functions $x \mapsto f(x) \sqcup g(x)$ and $x \mapsto f'(x) \sqcup g'(x)$ are also eventually equal with respect to $l$.

Filter.EventuallyEq.inf theorem

 [Min β] {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

Full source

theorem EventuallyEq.inf [Min β] {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 :=
  hf.comp₂ (· ⊓ ·) hg

Infimum Preserves Eventually Equal Functions under Filter

Informal description

Let $\beta$ be a type with a minimum operation $\sqcap$, and let $l$ be a filter on a type $\alpha$. For functions $f, f', g, g' : \alpha \to \beta$, if $f$ and $f'$ are eventually equal with respect to $l$ (i.e., $f(x) = f'(x)$ for all $x$ in some set in $l$), and $g$ and $g'$ are eventually equal with respect to $l$, then the functions $x \mapsto f(x) \sqcap g(x)$ and $x \mapsto f'(x) \sqcap g'(x)$ are also eventually equal with respect to $l$.

Filter.EventuallyEq.preimage theorem

{l : Filter α} {f g : α → β} (h : f =ᶠ[l] g) (s : Set β) : f ⁻¹' s =ᶠ[l] g ⁻¹' s

Full source

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

Preimage Preservation under Eventually Equal Functions

Informal description

Let $l$ be a filter on a type $\alpha$, and let $f, g : \alpha \to \beta$ be functions. If $f$ and $g$ are eventually equal with respect to $l$ (i.e., $f =ᶠ[l] g$), then for any subset $s \subseteq \beta$, the preimages $f^{-1}(s)$ and $g^{-1}(s)$ are also eventually equal with respect to $l$ (i.e., $f^{-1}(s) =ᶠ[l] g^{-1}(s)$).

Filter.EventuallyEq.inter theorem

 {s t s' t' : Set α} {l : Filter α} (h : s =ᶠ[l] t) (h' : s' =ᶠ[l] t') : (s ∩ s' : Set α) =ᶠ[l] (t ∩ t' : Set α)

Full source

theorem EventuallyEq.inter {s t s' t' : Set α} {l : Filter α} (h : s =ᶠ[l] t) (h' : s' =ᶠ[l] t') :
    (s ∩ s' : Set α) =ᶠ[l] (t ∩ t' : Set α) :=
  h.comp₂ (· ∧ ·) h'

Intersection Preserves Eventually Equal Sets under Filter

Informal description

Let $s, t, s', t'$ be sets in a type $\alpha$, and let $l$ be a filter on $\alpha$. If $s$ and $t$ are eventually equal with respect to $l$ (i.e., $s =ᶠ[l] t$), and $s'$ and $t'$ are eventually equal with respect to $l$ (i.e., $s' =ᶠ[l] t'$), then the intersections $s \cap s'$ and $t \cap t'$ are also eventually equal with respect to $l$ (i.e., $s \cap s' =ᶠ[l] t \cap t'$).

Filter.EventuallyEq.union theorem

 {s t s' t' : Set α} {l : Filter α} (h : s =ᶠ[l] t) (h' : s' =ᶠ[l] t') : (s ∪ s' : Set α) =ᶠ[l] (t ∪ t' : Set α)

Full source

theorem EventuallyEq.union {s t s' t' : Set α} {l : Filter α} (h : s =ᶠ[l] t) (h' : s' =ᶠ[l] t') :
    (s ∪ s' : Set α) =ᶠ[l] (t ∪ t' : Set α) :=
  h.comp₂ (· ∨ ·) h'

Union Preserves Eventually Equal Sets under Filter

Informal description

Let $s, t, s', t'$ be sets in a type $\alpha$, and let $l$ be a filter on $\alpha$. If $s$ and $t$ are eventually equal with respect to $l$ (i.e., $s =_l t$), and $s'$ and $t'$ are eventually equal with respect to $l$ (i.e., $s' =_l t'$), then their unions $s \cup s'$ and $t \cup t'$ are also eventually equal with respect to $l$ (i.e., $s \cup s' =_l t \cup t'$).

Filter.EventuallyEq.compl theorem

{s t : Set α} {l : Filter α} (h : s =ᶠ[l] t) : (sᶜ : Set α) =ᶠ[l] (tᶜ : Set α)

Full source

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

Complement Preserves Eventually Equal Sets

Informal description

Let $s$ and $t$ be sets in a type $\alpha$, and let $l$ be a filter on $\alpha$. If $s$ and $t$ are eventually equal with respect to $l$ (i.e., $s =ᶠ[l] t$), then their complements $s^c$ and $t^c$ are also eventually equal with respect to $l$ (i.e., $s^c =ᶠ[l] t^c$).

Filter.EventuallyEq.diff theorem

 {s t s' t' : Set α} {l : Filter α} (h : s =ᶠ[l] t) (h' : s' =ᶠ[l] t') : (s \ s' : Set α) =ᶠ[l] (t \ t' : Set α)

Full source

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

Set Difference Preserves Eventually Equal Sets under Filter

Informal description

Let $s, t, s', t'$ be sets in a type $\alpha$, and let $l$ be a filter on $\alpha$. If $s$ and $t$ are eventually equal with respect to $l$ (i.e., $s =_l t$), and $s'$ and $t'$ are eventually equal with respect to $l$ (i.e., $s' =_l t'$), then their set differences $s \setminus s'$ and $t \setminus t'$ are also eventually equal with respect to $l$ (i.e., $s \setminus s' =_l t \setminus t'$).

Filter.EventuallyEq.symmDiff theorem

 {s t s' t' : Set α} {l : Filter α} (h : s =ᶠ[l] t) (h' : s' =ᶠ[l] t') : (s ∆ s' : Set α) =ᶠ[l] (t ∆ t' : Set α)

Full source

protected theorem EventuallyEq.symmDiff {s t s' t' : Set α} {l : Filter α}
    (h : s =ᶠ[l] t) (h' : s' =ᶠ[l] t') : (s ∆ s' : Set α) =ᶠ[l] (t ∆ t' : Set α) :=
  (h.diff h').union (h'.diff h)

Symmetric Difference Preserves Eventually Equal Sets under Filter

Informal description

Let $s, t, s', t'$ be sets in a type $\alpha$, and let $l$ be a filter on $\alpha$. If $s$ and $t$ are eventually equal with respect to $l$ (i.e., $s =_l t$), and $s'$ and $t'$ are eventually equal with respect to $l$ (i.e., $s' =_l t'$), then their symmetric differences $s \triangle s'$ and $t \triangle t'$ are also eventually equal with respect to $l$ (i.e., $s \triangle s' =_l t \triangle t'$).

Filter.eventuallyEq_empty theorem

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

Full source

theorem eventuallyEq_empty {s : Set α} {l : Filter α} : s =ᶠ[l] (∅ : Set α)s =ᶠ[l] (∅ : Set α) ↔ ∀ᶠ x in l, x ∉ s :=
  eventuallyEq_set.trans <| by simp

Characterization of Eventually Empty Set via Non-Membership

Informal description

For any set $s$ in a type $\alpha$ and any filter $l$ on $\alpha$, the set $s$ is eventually equal to the empty set with respect to $l$ if and only if the condition $x \notin s$ holds for all $x$ in some set belonging to $l$. In other words: $$ s =_l \emptyset \iff \forall^l x, x \notin s $$

Filter.inter_eventuallyEq_left theorem

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

Full source

theorem inter_eventuallyEq_left {s t : Set α} {l : Filter α} :
    (s ∩ t : Set α) =ᶠ[l] s(s ∩ t : Set α) =ᶠ[l] s ↔ ∀ᶠ x in l, x ∈ s → x ∈ t := by
  simp only [eventuallyEq_set, mem_inter_iff, and_iff_left_iff_imp]

Intersection Eventually Equal to Left Operand iff Membership Implication Holds Eventually

Informal description

For any sets $s$ and $t$ in a type $\alpha$ and a filter $l$ on $\alpha$, the intersection $s \cap t$ is eventually equal to $s$ with respect to $l$ if and only if for all $x$ in some set belonging to $l$, whenever $x$ is in $s$, it is also in $t$. In other words: $$ s \cap t =_l s \iff \forall^l x, x \in s \to x \in t $$

Filter.inter_eventuallyEq_right theorem

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

Full source

theorem inter_eventuallyEq_right {s t : Set α} {l : Filter α} :
    (s ∩ t : Set α) =ᶠ[l] t(s ∩ t : Set α) =ᶠ[l] t ↔ ∀ᶠ x in l, x ∈ t → x ∈ s := by
  rw [inter_comm, inter_eventuallyEq_left]

Intersection Eventually Equal to Right Operand iff Reverse Membership Implication Holds Eventually

Informal description

For any sets $s$ and $t$ in a type $\alpha$ and a filter $l$ on $\alpha$, the intersection $s \cap t$ is eventually equal to $t$ with respect to $l$ if and only if for all $x$ in some set belonging to $l$, whenever $x$ is in $t$, it is also in $s$. In other words: $$ s \cap t =_l t \iff \forall^l x, x \in t \to x \in s $$

Filter.eventuallyEq_principal theorem

{s : Set α} {f g : α → β} : f =ᶠ[𝓟 s] g ↔ EqOn f g s

Full source

@[simp]
theorem eventuallyEq_principal {s : Set α} {f g : α → β} : f =ᶠ[𝓟 s] gf =ᶠ[𝓟 s] g ↔ EqOn f g s :=
  Iff.rfl

Equivalence of Eventually Equal on Principal Filter and Pointwise Equality on Set

Informal description

For any set $s \subseteq \alpha$ and functions $f, g : \alpha \to \beta$, the functions $f$ and $g$ are eventually equal with respect to the principal filter generated by $s$ if and only if $f$ and $g$ are equal on $s$. That is: $$ f =_{\mathfrak{P}(s)} g \leftrightarrow \forall x \in s, f(x) = g(x) $$

Filter.eventuallyEq_inf_principal_iff theorem

{F : Filter α} {s : Set α} {f g : α → β} : f =ᶠ[F ⊓ 𝓟 s] g ↔ ∀ᶠ x in F, x ∈ s → f x = g x

Full source

theorem eventuallyEq_inf_principal_iff {F : Filter α} {s : Set α} {f g : α → β} :
    f =ᶠ[F ⊓ 𝓟 s] gf =ᶠ[F ⊓ 𝓟 s] g ↔ ∀ᶠ x in F, x ∈ s → f x = g x :=
  eventually_inf_principal

Equivalence of Eventual Equality in Infimum Filter and Conditional Equality

Informal description

For a filter $F$ on a type $\alpha$, a subset $s \subseteq \alpha$, and functions $f, g : \alpha \to \beta$, the following are equivalent: 1. The functions $f$ and $g$ are eventually equal with respect to the filter $F \sqcap \mathfrak{P}(s)$ (where $\mathfrak{P}(s)$ is the principal filter generated by $s$). 2. The implication $x \in s \to f(x) = g(x)$ holds eventually for the filter $F$. In other words: $$ f =_{F \sqcap \mathfrak{P}(s)} g \iff \forall^F x, x \in s \to f(x) = g(x) $$

Filter.EventuallyEq.sub_eq theorem

[AddGroup β] {f g : α → β} {l : Filter α} (h : f =ᶠ[l] g) : f - g =ᶠ[l] 0

Full source

theorem EventuallyEq.sub_eq [AddGroup β] {f g : α → β} {l : Filter α} (h : f =ᶠ[l] g) :
    f - g =ᶠ[l] 0 := by simpa using ((EventuallyEq.refl l f).sub h).symm

Difference of Eventually Equal Functions Vanishes

Informal description

Let $\beta$ be an additive group. For any functions $f, g : \alpha \to \beta$ and any filter $l$ on $\alpha$, if $f$ and $g$ are eventually equal with respect to $l$, then their difference $f - g$ is eventually equal to the zero function with respect to $l$.

Filter.eventuallyEq_iff_sub theorem

[AddGroup β] {f g : α → β} {l : Filter α} : f =ᶠ[l] g ↔ f - g =ᶠ[l] 0

Full source

theorem eventuallyEq_iff_sub [AddGroup β] {f g : α → β} {l : Filter α} :
    f =ᶠ[l] gf =ᶠ[l] g ↔ f - g =ᶠ[l] 0 :=
  ⟨fun h => h.sub_eq, fun h => by simpa using h.add (EventuallyEq.refl l g)⟩

Characterization of Eventually Equal Functions via Vanishing Difference

Informal description

Let $\beta$ be an additive group. For any functions $f, g : \alpha \to \beta$ and any filter $l$ on $\alpha$, the functions $f$ and $g$ are eventually equal with respect to $l$ if and only if their difference $f - g$ is eventually equal to the zero function with respect to $l$. In other words: $$ f =^l g \iff f - g =^l 0 $$

Filter.eventuallyEq_iff_all_subsets theorem

{f g : α → β} {l : Filter α} : f =ᶠ[l] g ↔ ∀ s : Set α, ∀ᶠ x in l, x ∈ s → f x = g x

Full source

theorem eventuallyEq_iff_all_subsets {f g : α → β} {l : Filter α} :
    f =ᶠ[l] gf =ᶠ[l] g ↔ ∀ s : Set α, ∀ᶠ x in l, x ∈ s → f x = g x :=
  eventually_iff_all_subsets

Characterization of Eventually Equal Functions via All Subsets

Informal description

For any functions $f, g : \alpha \to \beta$ and any filter $l$ on $\alpha$, the following are equivalent: 1. $f$ and $g$ are eventually equal with respect to $l$ (i.e., $\{x \mid f(x) = g(x)\} \in l$). 2. For every subset $s \subseteq \alpha$, the implication "$x \in s$ implies $f(x) = g(x)$" holds eventually with respect to $l$ (i.e., $\{x \mid x \in s \to f(x) = g(x)\} \in l$ for all $s \subseteq \alpha$).

Filter.EventuallyLE.congr theorem

{f f' g g' : α → β} (H : f ≤ᶠ[l] g) (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') : f' ≤ᶠ[l] g'

Full source

theorem EventuallyLE.congr {f f' g g' : α → β} (H : f ≤ᶠ[l] g) (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') :
    f' ≤ᶠ[l] g' :=
  H.mp <| hg.mp <| hf.mono fun x hf hg H => by rwa [hf, hg] at H

Congruence of Eventually Less Than or Equal under Eventually Equal Functions

Informal description

Let $f, f', g, g' : \alpha \to \beta$ be functions and $l$ a filter on $\alpha$. If $f$ is eventually less than or equal to $g$ with respect to $l$ (i.e., $f \leqᶠ[l] g$), and $f$ is eventually equal to $f'$ (i.e., $f =ᶠ[l] f'$) and $g$ is eventually equal to $g'$ (i.e., $g =ᶠ[l] g'$) with respect to $l$, then $f'$ is eventually less than or equal to $g'$ with respect to $l$ (i.e., $f' \leqᶠ[l] g'$).

Filter.eventuallyLE_congr theorem

{f f' g g' : α → β} (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') : f ≤ᶠ[l] g ↔ f' ≤ᶠ[l] g'

Full source

theorem eventuallyLE_congr {f f' g g' : α → β} (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') :
    f ≤ᶠ[l] gf ≤ᶠ[l] g ↔ f' ≤ᶠ[l] g' :=
  ⟨fun H => H.congr hf hg, fun H => H.congr hf.symm hg.symm⟩

Equivalence of Eventual Inequalities under Eventual Equality

Informal description

For functions $f, f', g, g' : \alpha \to \beta$ and a filter $l$ on $\alpha$, if $f$ is eventually equal to $f'$ and $g$ is eventually equal to $g'$ with respect to $l$, then $f$ is eventually less than or equal to $g$ with respect to $l$ if and only if $f'$ is eventually less than or equal to $g'$ with respect to $l$. In other words: $$ f =ᶠ[l] f' \text{ and } g =ᶠ[l] g' \implies \left( f \leqᶠ[l] g \leftrightarrow f' \leqᶠ[l] g' \right). $$

Filter.eventuallyLE_iff_all_subsets theorem

{f g : α → β} {l : Filter α} : f ≤ᶠ[l] g ↔ ∀ s : Set α, ∀ᶠ x in l, x ∈ s → f x ≤ g x

Full source

theorem eventuallyLE_iff_all_subsets {f g : α → β} {l : Filter α} :
    f ≤ᶠ[l] gf ≤ᶠ[l] g ↔ ∀ s : Set α, ∀ᶠ x in l, x ∈ s → f x ≤ g x :=
  eventually_iff_all_subsets

Characterization of Eventually Less Than or Equal via All Subsets

Informal description

For functions $f, g : \alpha \to \beta$ and a filter $l$ on $\alpha$, the following are equivalent: 1. $f$ is eventually less than or equal to $g$ with respect to $l$ (i.e., $\{x \mid f(x) \leq g(x)\} \in l$). 2. For every subset $s \subseteq \alpha$, the implication "$x \in s$ implies $f(x) \leq g(x)$" holds eventually with respect to $l$ (i.e., $\{x \mid x \in s \to f(x) \leq g(x)\} \in l$ for all $s \subseteq \alpha$).

Filter.EventuallyEq.le theorem

(h : f =ᶠ[l] g) : f ≤ᶠ[l] g

Full source

theorem EventuallyEq.le (h : f =ᶠ[l] g) : f ≤ᶠ[l] g :=
  h.mono fun _ => le_of_eq

Eventual Equality Implies Eventual Inequality: $f =ᶠ[l] g \implies f \leqᶠ[l] g$

Informal description

Let $f, g : \alpha \to \beta$ be functions and $l$ a filter on $\alpha$. If $f$ and $g$ are eventually equal with respect to $l$ (i.e., $\{x \mid f(x) = g(x)\} \in l$), then $f$ is eventually less than or equal to $g$ with respect to $l$ (i.e., $\{x \mid f(x) \leq g(x)\} \in l$).

Filter.EventuallyLE.refl theorem

(l : Filter α) (f : α → β) : f ≤ᶠ[l] f

Full source

@[refl]
theorem EventuallyLE.refl (l : Filter α) (f : α → β) : f ≤ᶠ[l] f :=
  EventuallyEq.rfl.le

Reflexivity of the Eventually Less-Than-or-Equal Relation under a Filter

Informal description

For any filter $l$ on a type $\alpha$ and any function $f : \alpha \to \beta$ (where $\beta$ has a preorder), the function $f$ is eventually less than or equal to itself with respect to $l$. That is, the set $\{x \in \alpha \mid f(x) \leq f(x)\}$ belongs to the filter $l$.

Filter.EventuallyLE.rfl theorem

: f ≤ᶠ[l] f

Full source

theorem EventuallyLE.rfl : f ≤ᶠ[l] f :=
  EventuallyLE.refl l f

Reflexivity of Eventual Inequality: $f \leqᶠ[l] f$

Informal description

For any filter $l$ on a type $\alpha$ and any function $f : \alpha \to \beta$ (where $\beta$ has a preorder), the relation $f \leqᶠ[l] f$ holds. That is, the set $\{x \in \alpha \mid f(x) \leq f(x)\}$ belongs to the filter $l$.

Filter.EventuallyLE.trans theorem

(H₁ : f ≤ᶠ[l] g) (H₂ : g ≤ᶠ[l] h) : f ≤ᶠ[l] h

Full source

@[trans]
theorem EventuallyLE.trans (H₁ : f ≤ᶠ[l] g) (H₂ : g ≤ᶠ[l] h) : f ≤ᶠ[l] h :=
  H₂.mp <| H₁.mono fun _ => le_trans

Transitivity of Eventually Less-Than-or-Equal Relation under a Filter

Informal description

Let $l$ be a filter on a type $\alpha$, and let $f, g, h : \alpha \to \beta$ be functions where $\beta$ has a preorder. If $f \leqᶠ[l] g$ (i.e., $f(x) \leq g(x)$ eventually in $l$) and $g \leqᶠ[l] h$ (i.e., $g(x) \leq h(x)$ eventually in $l$), then $f \leqᶠ[l] h$ (i.e., $f(x) \leq h(x)$ eventually in $l$).

Filter.instTransForallEventuallyLE instance

: Trans ((· ≤ᶠ[l] ·) : (α → β) → (α → β) → Prop) (· ≤ᶠ[l] ·) (· ≤ᶠ[l] ·)

Full source

instance : Trans ((· ≤ᶠ[l] ·) : (α → β) → (α → β) → Prop) (· ≤ᶠ[l] ·) (· ≤ᶠ[l] ·) where
  trans := EventuallyLE.trans

Transitivity of Eventually Less-Than-or-Equal Relation under a Filter

Informal description

The relation $\leqᶠ[l]$ on functions $\alpha \to \beta$ (for a preorder $\beta$) is transitive. That is, for any filter $l$ on $\alpha$ and functions $f, g, h : \alpha \to \beta$, if $f \leqᶠ[l] g$ and $g \leqᶠ[l] h$, then $f \leqᶠ[l] h$.

Filter.EventuallyEq.trans_le theorem

(H₁ : f =ᶠ[l] g) (H₂ : g ≤ᶠ[l] h) : f ≤ᶠ[l] h

Full source

@[trans]
theorem EventuallyEq.trans_le (H₁ : f =ᶠ[l] g) (H₂ : g ≤ᶠ[l] h) : f ≤ᶠ[l] h :=
  H₁.le.trans H₂

Transitivity of Eventual Equality and Inequality under a Filter: $f =ᶠ[l] g \land g \leqᶠ[l] h \implies f \leqᶠ[l] h$

Informal description

Let $l$ be a filter on a type $\alpha$, and let $f, g, h : \alpha \to \beta$ be functions where $\beta$ has a preorder. If $f$ and $g$ are eventually equal with respect to $l$ (i.e., $f(x) = g(x)$ for all $x$ in some set in $l$) and $g$ is eventually less than or equal to $h$ with respect to $l$ (i.e., $g(x) \leq h(x)$ for all $x$ in some set in $l$), then $f$ is eventually less than or equal to $h$ with respect to $l$ (i.e., $f(x) \leq h(x)$ for all $x$ in some set in $l$).

Filter.instTransForallEventuallyEqEventuallyLE instance

: Trans ((· =ᶠ[l] ·) : (α → β) → (α → β) → Prop) (· ≤ᶠ[l] ·) (· ≤ᶠ[l] ·)

Full source

instance : Trans ((· =ᶠ[l] ·) : (α → β) → (α → β) → Prop) (· ≤ᶠ[l] ·) (· ≤ᶠ[l] ·) where
  trans := EventuallyEq.trans_le

Transitivity of Eventual Equality and Inequality under a Filter

Informal description

For any filter $l$ on a type $\alpha$ and functions $f, g, h : \alpha \to \beta$ where $\beta$ has a preorder, if $f$ is eventually equal to $g$ with respect to $l$ and $g$ is eventually less than or equal to $h$ with respect to $l$, then $f$ is eventually less than or equal to $h$ with respect to $l$.

Filter.EventuallyLE.trans_eq theorem

(H₁ : f ≤ᶠ[l] g) (H₂ : g =ᶠ[l] h) : f ≤ᶠ[l] h

Full source

@[trans]
theorem EventuallyLE.trans_eq (H₁ : f ≤ᶠ[l] g) (H₂ : g =ᶠ[l] h) : f ≤ᶠ[l] h :=
  H₁.trans H₂.le

Transitivity of Eventual Inequality with Eventual Equality: $f \leqᶠ[l] g$ and $g =ᶠ[l] h$ implies $f \leqᶠ[l] h$

Informal description

Let $l$ be a filter on a type $\alpha$, and let $f, g, h : \alpha \to \beta$ be functions where $\beta$ has a preorder. If $f \leqᶠ[l] g$ (i.e., $f(x) \leq g(x)$ for all $x$ in some set in $l$) and $g =ᶠ[l] h$ (i.e., $g(x) = h(x)$ for all $x$ in some set in $l$), then $f \leqᶠ[l] h$ (i.e., $f(x) \leq h(x)$ for all $x$ in some set in $l$).

Filter.instTransForallEventuallyLEEventuallyEq instance

: Trans ((· ≤ᶠ[l] ·) : (α → β) → (α → β) → Prop) (· =ᶠ[l] ·) (· ≤ᶠ[l] ·)

Full source

instance : Trans ((· ≤ᶠ[l] ·) : (α → β) → (α → β) → Prop) (· =ᶠ[l] ·) (· ≤ᶠ[l] ·) where
  trans := EventuallyLE.trans_eq

Transitivity of Eventual Inequality with Respect to Eventual Equality

Informal description

For any type $\alpha$ with a filter $l$ and any type $\beta$ with a preorder, the relation $\leqᶠ[l]$ is transitive with respect to $=ᶠ[l]$. That is, if $f \leqᶠ[l] g$ and $g =ᶠ[l] h$, then $f \leqᶠ[l] h$.

Filter.EventuallyLE.antisymm theorem

[PartialOrder β] {l : Filter α} {f g : α → β} (h₁ : f ≤ᶠ[l] g) (h₂ : g ≤ᶠ[l] f) : f =ᶠ[l] g

Full source

theorem EventuallyLE.antisymm [PartialOrder β] {l : Filter α} {f g : α → β} (h₁ : f ≤ᶠ[l] g)
    (h₂ : g ≤ᶠ[l] f) : f =ᶠ[l] g :=
  h₂.mp <| h₁.mono fun _ => le_antisymm

Antisymmetry of Eventually Less-Than-Or-Equal Relation for Filters

Informal description

Let $\beta$ be a partially ordered set, $l$ a filter on a type $\alpha$, and $f, g : \alpha \to \beta$ two functions. If $f$ is eventually less than or equal to $g$ with respect to $l$ (i.e., $f \leqᶠ[l] g$) and $g$ is eventually less than or equal to $f$ with respect to $l$ (i.e., $g \leqᶠ[l] f$), then $f$ and $g$ are eventually equal with respect to $l$ (i.e., $f =ᶠ[l] g$).

Filter.eventuallyLE_antisymm_iff theorem

[PartialOrder β] {l : Filter α} {f g : α → β} : f =ᶠ[l] g ↔ f ≤ᶠ[l] g ∧ g ≤ᶠ[l] f

Full source

theorem eventuallyLE_antisymm_iff [PartialOrder β] {l : Filter α} {f g : α → β} :
    f =ᶠ[l] gf =ᶠ[l] g ↔ f ≤ᶠ[l] g ∧ g ≤ᶠ[l] f := by
  simp only [EventuallyEq, EventuallyLE, le_antisymm_iff, eventually_and]

Antisymmetry of Eventually Equal Functions in Partial Order

Informal description

Let $\beta$ be a partially ordered set, $l$ a filter on a type $\alpha$, and $f, g : \alpha \to \beta$ two functions. Then $f$ and $g$ are eventually equal with respect to $l$ if and only if both $f$ is eventually less than or equal to $g$ and $g$ is eventually less than or equal to $f$ with respect to $l$. In other words: $$ f =ᶠ[l] g \leftrightarrow (f \leqᶠ[l] g) \land (g \leqᶠ[l] f) $$

Filter.EventuallyLE.le_iff_eq theorem

[PartialOrder β] {l : Filter α} {f g : α → β} (h : f ≤ᶠ[l] g) : g ≤ᶠ[l] f ↔ g =ᶠ[l] f

Full source

theorem EventuallyLE.le_iff_eq [PartialOrder β] {l : Filter α} {f g : α → β} (h : f ≤ᶠ[l] g) :
    g ≤ᶠ[l] fg ≤ᶠ[l] f ↔ g =ᶠ[l] f :=
  ⟨fun h' => h'.antisymm h, EventuallyEq.le⟩

Antisymmetry Criterion for Eventually Less-Than-Or-Equal Functions

Informal description

Let $\beta$ be a partially ordered set, $l$ a filter on a type $\alpha$, and $f, g : \alpha \to \beta$ two functions such that $f \leqᶠ[l] g$. Then $g \leqᶠ[l] f$ holds if and only if $g =ᶠ[l] f$.

Filter.Eventually.ne_of_lt theorem

[Preorder β] {l : Filter α} {f g : α → β} (h : ∀ᶠ x in l, f x < g x) : ∀ᶠ x in l, f x ≠ g x

Full source

theorem Eventually.ne_of_lt [Preorder β] {l : Filter α} {f g : α → β} (h : ∀ᶠ x in l, f x < g x) :
    ∀ᶠ x in l, f x ≠ g x :=
  h.mono fun _ hx => hx.ne

Eventual Strict Inequality Implies Eventual Non-Equality in Preorders

Informal description

Let $\beta$ be a preordered set, $l$ a filter on a type $\alpha$, and $f, g : \alpha \to \beta$ two functions. If $f(x) < g(x)$ holds eventually in $l$, then $f(x) \neq g(x)$ also holds eventually in $l$. In other words: $$ (\forallᶠ x \text{ in } l, f(x) < g(x)) \implies (\forallᶠ x \text{ in } l, f(x) \neq g(x)) $$

Filter.Eventually.ne_top_of_lt theorem

 [Preorder β] [OrderTop β] {l : Filter α} {f g : α → β} (h : ∀ᶠ x in l, f x < g x) : ∀ᶠ x in l, f x ≠ ⊤

Full source

theorem Eventually.ne_top_of_lt [Preorder β] [OrderTop β] {l : Filter α} {f g : α → β}
    (h : ∀ᶠ x in l, f x < g x) : ∀ᶠ x in l, f x ≠ ⊤ :=
  h.mono fun _ hx => hx.ne_top

Eventual Strict Inequality Implies Eventual Non-Top Element

Informal description

Let $\beta$ be a type with a preorder and a greatest element $\top$, and let $l$ be a filter on a type $\alpha$. For functions $f, g : \alpha \to \beta$, if $f(x) < g(x)$ holds eventually in $l$, then $f(x) \neq \top$ also holds eventually in $l$.

Filter.Eventually.lt_top_of_ne theorem

 [PartialOrder β] [OrderTop β] {l : Filter α} {f : α → β} (h : ∀ᶠ x in l, f x ≠ ⊤) : ∀ᶠ x in l, f x < ⊤

Full source

theorem Eventually.lt_top_of_ne [PartialOrder β] [OrderTop β] {l : Filter α} {f : α → β}
    (h : ∀ᶠ x in l, f x ≠ ⊤) : ∀ᶠ x in l, f x < ⊤ :=
  h.mono fun _ hx => hx.lt_top

Eventual Strict Upper Bound for Non-Top Values: $\forallᶠ x \text{ in } l, f(x) \neq \top \to \forallᶠ x \text{ in } l, f(x) < \top$

Informal description

Let $\beta$ be a partially ordered type with a top element $\top$, and let $l$ be a filter on a type $\alpha$. For a function $f : \alpha \to \beta$, if $f(x) \neq \top$ holds eventually in $l$ (i.e., $\forallᶠ x \text{ in } l, f(x) \neq \top$), then $f(x) < \top$ also holds eventually in $l$ (i.e., $\forallᶠ x \text{ in } l, f(x) < \top$).

Filter.Eventually.lt_top_iff_ne_top theorem

 [PartialOrder β] [OrderTop β] {l : Filter α} {f : α → β} : (∀ᶠ x in l, f x < ⊤) ↔ ∀ᶠ x in l, f x ≠ ⊤

Full source

theorem Eventually.lt_top_iff_ne_top [PartialOrder β] [OrderTop β] {l : Filter α} {f : α → β} :
    (∀ᶠ x in l, f x < ⊤) ↔ ∀ᶠ x in l, f x ≠ ⊤ :=
  ⟨Eventually.ne_of_lt, Eventually.lt_top_of_ne⟩

Equivalence of Eventual Strict Upper Bound and Non-Top Condition

Informal description

Let $\beta$ be a partially ordered set with a greatest element $\top$, and let $l$ be a filter on a type $\alpha$. For a function $f : \alpha \to \beta$, the following are equivalent: 1. $f(x) < \top$ holds eventually in $l$ (i.e., $\forallᶠ x \text{ in } l, f(x) < \top$) 2. $f(x) \neq \top$ holds eventually in $l$ (i.e., $\forallᶠ x \text{ in } l, f(x) \neq \top$) In other words: $$ (\forallᶠ x \text{ in } l, f(x) < \top) \leftrightarrow (\forallᶠ x \text{ in } l, f(x) \neq \top) $$

Filter.EventuallyLE.inter theorem

 {s t s' t' : Set α} {l : Filter α} (h : s ≤ᶠ[l] t) (h' : s' ≤ᶠ[l] t') : (s ∩ s' : Set α) ≤ᶠ[l] (t ∩ t' : Set α)

Full source

@[mono]
theorem EventuallyLE.inter {s t s' t' : Set α} {l : Filter α} (h : s ≤ᶠ[l] t) (h' : s' ≤ᶠ[l] t') :
    (s ∩ s' : Set α) ≤ᶠ[l] (t ∩ t' : Set α) :=
  h'.mp <| h.mono fun _ => And.imp

Intersection Preserves Eventual Subset Relation under a Filter

Informal description

Let $l$ be a filter on a type $\alpha$, and let $s, t, s', t'$ be subsets of $\alpha$. If $s \leqᶠ[l] t$ (i.e., the set $\{x \mid x \in s \to x \in t\}$ is in $l$) and $s' \leqᶠ[l] t'$, then the intersection $s \cap s'$ is eventually less than or equal to $t \cap t'$ with respect to $l$, i.e., $(s \cap s') \leqᶠ[l] (t \cap t')$.

Filter.EventuallyLE.union theorem

 {s t s' t' : Set α} {l : Filter α} (h : s ≤ᶠ[l] t) (h' : s' ≤ᶠ[l] t') : (s ∪ s' : Set α) ≤ᶠ[l] (t ∪ t' : Set α)

Full source

@[mono]
theorem EventuallyLE.union {s t s' t' : Set α} {l : Filter α} (h : s ≤ᶠ[l] t) (h' : s' ≤ᶠ[l] t') :
    (s ∪ s' : Set α) ≤ᶠ[l] (t ∪ t' : Set α) :=
  h'.mp <| h.mono fun _ => Or.imp

Union Preserves Eventually Less-Than-Or-Equal Relation under a Filter

Informal description

Let $l$ be a filter on a type $\alpha$, and let $s, t, s', t'$ be subsets of $\alpha$. If $s$ is eventually less than or equal to $t$ with respect to $l$ (i.e., $s \leqᶠ[l] t$) and $s'$ is eventually less than or equal to $t'$ with respect to $l$ (i.e., $s' \leqᶠ[l] t'$), then the union $s \cup s'$ is eventually less than or equal to the union $t \cup t'$ with respect to $l$ (i.e., $s \cup s' \leqᶠ[l] t \cup t'$).

Filter.EventuallyLE.compl theorem

{s t : Set α} {l : Filter α} (h : s ≤ᶠ[l] t) : (tᶜ : Set α) ≤ᶠ[l] (sᶜ : Set α)

Full source

@[mono]
theorem EventuallyLE.compl {s t : Set α} {l : Filter α} (h : s ≤ᶠ[l] t) :
    (tᶜ : Set α) ≤ᶠ[l] (sᶜ : Set α) :=
  h.mono fun _ => mt

Complement Reversal in Eventually Contained Sets

Informal description

Let $s$ and $t$ be subsets of a type $\alpha$, and let $l$ be a filter on $\alpha$. If $s$ is eventually contained in $t$ with respect to $l$ (i.e., the set $\{x \mid x \in s \rightarrow x \in t\}$ belongs to $l$), then the complement $t^c$ is eventually contained in the complement $s^c$ with respect to $l$.

Filter.EventuallyLE.diff theorem

 {s t s' t' : Set α} {l : Filter α} (h : s ≤ᶠ[l] t) (h' : t' ≤ᶠ[l] s') : (s \ s' : Set α) ≤ᶠ[l] (t \ t' : Set α)

Full source

@[mono]
theorem EventuallyLE.diff {s t s' t' : Set α} {l : Filter α} (h : s ≤ᶠ[l] t) (h' : t' ≤ᶠ[l] s') :
    (s \ s' : Set α) ≤ᶠ[l] (t \ t' : Set α) :=
  h.inter h'.compl

Set Difference Preserves Eventual Subset Relation under a Filter

Informal description

Let $l$ be a filter on a type $\alpha$, and let $s, t, s', t'$ be subsets of $\alpha$. If $s$ is eventually less than or equal to $t$ with respect to $l$ (i.e., $s \leqᶠ[l] t$) and $t'$ is eventually less than or equal to $s'$ with respect to $l$ (i.e., $t' \leqᶠ[l] s'$), then the set difference $s \setminus s'$ is eventually less than or equal to $t \setminus t'$ with respect to $l$ (i.e., $s \setminus s' \leqᶠ[l] t \setminus t'$).

Filter.set_eventuallyLE_iff_mem_inf_principal theorem

{s t : Set α} {l : Filter α} : s ≤ᶠ[l] t ↔ t ∈ l ⊓ 𝓟 s

Full source

theorem set_eventuallyLE_iff_mem_inf_principal {s t : Set α} {l : Filter α} :
    s ≤ᶠ[l] ts ≤ᶠ[l] t ↔ t ∈ l ⊓ 𝓟 s :=
  eventually_inf_principal.symm

Characterization of Eventually Contained Sets via Infimum with Principal Filter

Informal description

For any sets $s, t \subseteq \alpha$ and any filter $l$ on $\alpha$, the following are equivalent: 1. The set $\{x \mid x \in s \to x \in t\}$ belongs to $l$ (i.e., $s$ is eventually contained in $t$ with respect to $l$). 2. The set $t$ belongs to the infimum filter $l \sqcap \mathfrak{P}(s)$, where $\mathfrak{P}(s)$ is the principal filter generated by $s$. In other words, $s \leqᶠ[l] t$ if and only if $t \in l \sqcap \mathfrak{P}(s)$.

Filter.set_eventuallyLE_iff_inf_principal_le theorem

{s t : Set α} {l : Filter α} : s ≤ᶠ[l] t ↔ l ⊓ 𝓟 s ≤ l ⊓ 𝓟 t

Full source

theorem set_eventuallyLE_iff_inf_principal_le {s t : Set α} {l : Filter α} :
    s ≤ᶠ[l] ts ≤ᶠ[l] t ↔ l ⊓ 𝓟 s ≤ l ⊓ 𝓟 t :=
  set_eventuallyLE_iff_mem_inf_principal.trans <| by
    simp only [le_inf_iff, inf_le_left, true_and, le_principal_iff]

Characterization of Eventually Contained Sets via Infimum Comparison of Principal Filters

Informal description

For any sets $s, t \subseteq \alpha$ and any filter $l$ on $\alpha$, the following are equivalent: 1. The set $\{x \mid x \in s \to x \in t\}$ belongs to $l$ (i.e., $s$ is eventually contained in $t$ with respect to $l$). 2. The infimum of $l$ with the principal filter generated by $s$ is less than or equal to the infimum of $l$ with the principal filter generated by $t$. In other words, $s \leqᶠ[l] t$ if and only if $l \sqcap \mathfrak{P}(s) \leq l \sqcap \mathfrak{P}(t)$, where $\mathfrak{P}(s)$ denotes the principal filter generated by $s$.

Filter.set_eventuallyEq_iff_inf_principal theorem

{s t : Set α} {l : Filter α} : s =ᶠ[l] t ↔ l ⊓ 𝓟 s = l ⊓ 𝓟 t

Full source

theorem set_eventuallyEq_iff_inf_principal {s t : Set α} {l : Filter α} :
    s =ᶠ[l] ts =ᶠ[l] t ↔ l ⊓ 𝓟 s = l ⊓ 𝓟 t := by
  simp only [eventuallyLE_antisymm_iff, le_antisymm_iff, set_eventuallyLE_iff_inf_principal_le]

Characterization of Eventually Equal Sets via Infimum with Principal Filters

Informal description

For any sets $s, t \subseteq \alpha$ and any filter $l$ on $\alpha$, the sets $s$ and $t$ are eventually equal with respect to $l$ (i.e., $\{x \mid x \in s \leftrightarrow x \in t\} \in l$) if and only if the infimum of $l$ with the principal filter generated by $s$ is equal to the infimum of $l$ with the principal filter generated by $t$.

Filter.EventuallyLE.sup theorem

 [SemilatticeSup β] {l : Filter α} {f₁ f₂ g₁ g₂ : α → β} (hf : f₁ ≤ᶠ[l] f₂) (hg : g₁ ≤ᶠ[l] g₂) : f₁ ⊔ g₁ ≤ᶠ[l] f₂ ⊔ g₂

Full source

theorem EventuallyLE.sup [SemilatticeSup β] {l : Filter α} {f₁ f₂ g₁ g₂ : α → β} (hf : f₁ ≤ᶠ[l] f₂)
    (hg : g₁ ≤ᶠ[l] g₂) : f₁ ⊔ g₁f₁ ⊔ g₁ ≤ᶠ[l] f₂ ⊔ g₂ := by
  filter_upwards [hf, hg] with x hfx hgx using sup_le_sup hfx hgx

Pointwise Supremum Preserves Eventual Inequality in Filters

Informal description

Let $\beta$ be a join-semilattice, $l$ a filter on a type $\alpha$, and $f_1, f_2, g_1, g_2 : \alpha \to \beta$ functions. If $f_1 \leqᶠ[l] f_2$ and $g_1 \leqᶠ[l] g_2$ (i.e., $f_1(x) \leq f_2(x)$ and $g_1(x) \leq g_2(x)$ hold eventually for $x$ in $l$), then the pointwise supremum $f_1 \sqcup g_1 \leqᶠ[l] f_2 \sqcup g_2$ holds eventually in $l$.

Filter.EventuallyLE.sup_le theorem

[SemilatticeSup β] {l : Filter α} {f g h : α → β} (hf : f ≤ᶠ[l] h) (hg : g ≤ᶠ[l] h) : f ⊔ g ≤ᶠ[l] h

Full source

theorem EventuallyLE.sup_le [SemilatticeSup β] {l : Filter α} {f g h : α → β} (hf : f ≤ᶠ[l] h)
    (hg : g ≤ᶠ[l] h) : f ⊔ gf ⊔ g ≤ᶠ[l] h := by
  filter_upwards [hf, hg] with x hfx hgx using _root_.sup_le hfx hgx

Supremum of Eventually Bounded Functions is Eventually Bounded

Informal description

Let $\beta$ be a join-semilattice, $l$ a filter on a type $\alpha$, and $f, g, h : \alpha \to \beta$ functions. If $f$ is eventually less than or equal to $h$ with respect to $l$ (i.e., $\{x \mid f(x) \leq h(x)\} \in l$) and $g$ is eventually less than or equal to $h$ with respect to $l$, then the pointwise supremum $f \sqcup g$ is eventually less than or equal to $h$ with respect to $l$.

Filter.EventuallyLE.le_sup_of_le_left theorem

[SemilatticeSup β] {l : Filter α} {f g h : α → β} (hf : h ≤ᶠ[l] f) : h ≤ᶠ[l] f ⊔ g

Full source

theorem EventuallyLE.le_sup_of_le_left [SemilatticeSup β] {l : Filter α} {f g h : α → β}
    (hf : h ≤ᶠ[l] f) : h ≤ᶠ[l] f ⊔ g :=
  hf.mono fun _ => _root_.le_sup_of_le_left

Left Eventual Inequality Implies Supremum Inequality under a Filter

Informal description

Let $\beta$ be a join-semilattice, $l$ a filter on a type $\alpha$, and $f, g, h : \alpha \to \beta$ functions. If $h \leqᶠ[l] f$ (i.e., $h(x) \leq f(x)$ holds eventually for $x$ in $l$), then $h \leqᶠ[l] f \sqcup g$ holds eventually in $l$.

Filter.EventuallyLE.le_sup_of_le_right theorem

[SemilatticeSup β] {l : Filter α} {f g h : α → β} (hg : h ≤ᶠ[l] g) : h ≤ᶠ[l] f ⊔ g

Full source

theorem EventuallyLE.le_sup_of_le_right [SemilatticeSup β] {l : Filter α} {f g h : α → β}
    (hg : h ≤ᶠ[l] g) : h ≤ᶠ[l] f ⊔ g :=
  hg.mono fun _ => _root_.le_sup_of_le_right

Right Inequality Implies Supremum Inequality for Eventually Bounded Functions

Informal description

Let $\beta$ be a join-semilattice, $l$ a filter on a type $\alpha$, and $f, g, h : \alpha \to \beta$ functions. If $h$ is eventually less than or equal to $g$ with respect to $l$ (i.e., $\{x \mid h(x) \leq g(x)\} \in l$), then $h$ is eventually less than or equal to the pointwise supremum $f \sqcup g$ with respect to $l$.

Filter.join_le theorem

{f : Filter (Filter α)} {l : Filter α} (h : ∀ᶠ m in f, m ≤ l) : join f ≤ l

Full source

theorem join_le {f : Filter (Filter α)} {l : Filter α} (h : ∀ᶠ m in f, m ≤ l) : join f ≤ l :=
  fun _ hs => h.mono fun _ hm => hm hs

Join of Filters is Bounded by Pointwise Bounds

Informal description

Let $f$ be a filter on the space of filters on a type $\alpha$, and let $l$ be a filter on $\alpha$. If for eventually every filter $m$ in $f$ we have $m \leq l$, then the join of $f$ is less than or equal to $l$.

Set.EqOn.eventuallyEq theorem

{α β} {s : Set α} {f g : α → β} (h : EqOn f g s) : f =ᶠ[𝓟 s] g

Full source

theorem Set.EqOn.eventuallyEq {α β} {s : Set α} {f g : α → β} (h : EqOn f g s) : f =ᶠ[𝓟 s] g :=
  h

Equality on a Set Implies Eventual Equality under Principal Filter

Informal description

For any set $s \subseteq \alpha$ and any two functions $f, g : \alpha \to \beta$, if $f$ and $g$ are equal on $s$ (i.e., $f(x) = g(x)$ for all $x \in s$), then $f$ and $g$ are eventually equal with respect to the principal filter generated by $s$.

Set.EqOn.eventuallyEq_of_mem theorem

{α β} {s : Set α} {l : Filter α} {f g : α → β} (h : EqOn f g s) (hl : s ∈ l) : f =ᶠ[l] g

Full source

theorem Set.EqOn.eventuallyEq_of_mem {α β} {s : Set α} {l : Filter α} {f g : α → β} (h : EqOn f g s)
    (hl : s ∈ l) : f =ᶠ[l] g :=
  h.eventuallyEq.filter_mono <| Filter.le_principal_iff.2 hl

Equality on a Filter Member Implies Eventual Equality

Informal description

For any set $s \subseteq \alpha$, any filter $l$ on $\alpha$, and any two functions $f, g : \alpha \to \beta$, if $f$ and $g$ are equal on $s$ (i.e., $f(x) = g(x)$ for all $x \in s$) and $s$ belongs to $l$, then $f$ and $g$ are eventually equal with respect to $l$.

HasSubset.Subset.eventuallyLE theorem

{α} {l : Filter α} {s t : Set α} (h : s ⊆ t) : s ≤ᶠ[l] t

Full source

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

Subset Implies Eventually Less Than or Equal Under Any Filter

Informal description

For any filter $l$ on a type $\alpha$ and any two sets $s, t \subseteq \alpha$, if $s \subseteq t$, then $s$ is eventually less than or equal to $t$ with respect to $l$, i.e., $\{x \mid x \in s \to x \in t\} \in l$.

Filter.compl_mem_comk theorem

{p : Set α → Prop} {he hmono hunion s} : sᶜ ∈ comk p he hmono hunion ↔ p s

Full source

lemma compl_mem_comk {p : Set α → Prop} {he hmono hunion s} :
    sᶜsᶜ ∈ comk p he hmono hunionsᶜ ∈ comk p he hmono hunion ↔ p s := by
  simp

Complement Membership in Filter Generated by Predicate

Informal description

For any predicate $ p $ on subsets of a type $ \alpha $ satisfying: 1. $ p(\emptyset) $ holds, 2. $ p $ is monotone (if $ p(t) $ holds and $ s \subseteq t $, then $ p(s) $ holds), 3. $ p $ is stable under finite unions (if $ p(s) $ and $ p(t) $ hold, then $ p(s \cup t) $ holds), a subset $ s $ of $ \alpha $ has its complement $ s^c $ in the filter generated by $ p $ if and only if $ p(s) $ holds. In other words, $ s^c \in \text{comk } p \text{ he hmono hunion} \leftrightarrow p(s) $.

Mathlib.Order.Filter.Basic

Main definitions

Notations

References