Mathlib.Order.Filter.Defs

Filter structure

(α : Type*)

Full source

/-- A filter `F` on a type `α` is a collection of sets of `α` which contains the whole `α`,
is upwards-closed, and is stable under intersection. We do not forbid this collection to be
all sets of `α`. -/
structure Filter (α : Type*) where
  /-- The set of sets that belong to the filter. -/
  sets : Set (Set α)
  /-- The set `Set.univ` belongs to any filter. -/
  univ_sets : Set.univSet.univ ∈ sets
  /-- If a set belongs to a filter, then its superset belongs to the filter as well. -/
  sets_of_superset {x y} : x ∈ sets → x ⊆ y → y ∈ sets
  /-- If two sets belong to a filter, then their intersection belongs to the filter as well. -/
  inter_sets {x y} : x ∈ sets → y ∈ sets → x ∩ yx ∩ y ∈ sets

Filter on a Type

Informal description

A filter $F$ on a type $\alpha$ is a collection of subsets of $\alpha$ that satisfies the following properties: 1. The entire set $\alpha$ is in $F$. 2. If a set $s$ is in $F$ and $s \subseteq t$, then $t$ is also in $F$ (upwards-closed). 3. If two sets $s$ and $t$ are in $F$, then their intersection $s \cap t$ is also in $F$ (stable under intersection). Unlike Bourbaki's definition, we do not require that $F$ cannot be the collection of all subsets of $\alpha$.

Filter.filter_eq theorem

: ∀ {f g : Filter α}, f.sets = g.sets → f = g

Full source

theorem filter_eq : ∀ {f g : Filter α}, f.sets = g.sets → f = g
  | ⟨_, _, _, _⟩, ⟨_, _, _, _⟩, rfl => rfl

Equality of Filters via Set Equality

Informal description

For any two filters $f$ and $g$ on a type $\alpha$, if the collections of sets belonging to $f$ and $g$ are equal (i.e., $f.\text{sets} = g.\text{sets}$), then $f = g$.

Filter.instMembership instance

: Membership (Set α) (Filter α)

Full source

/-- If `F` is a filter on `α`, and `U` a subset of `α` then we can write `U ∈ F` as on paper. -/
instance instMembership : Membership (Set α) (Filter α) := ⟨fun F U => U ∈ F.sets⟩

Membership Relation for Filters

Informal description

For any type $\alpha$, a filter $F$ on $\alpha$ has a membership relation $\in$ where $U \in F$ means the subset $U$ of $\alpha$ belongs to the filter $F$.

Filter.ext theorem

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

Full source

@[ext]
protected theorem ext (h : ∀ s, s ∈ fs ∈ f ↔ s ∈ g) : f = g := filter_eq <| Set.ext h

Extensionality of Filters: $f = g \iff \forall s, s \in f \leftrightarrow s \in g$

Informal description

For any two filters $f$ and $g$ on a type $\alpha$, if for every subset $s$ of $\alpha$ we have $s \in f$ if and only if $s \in g$, then $f = g$.

Filter.mem_mk theorem

{t : Set (Set α)} {h₁ h₂ h₃} : s ∈ mk t h₁ h₂ h₃ ↔ s ∈ t

Full source

@[simp]
protected theorem mem_mk {t : Set (Set α)} {h₁ h₂ h₃} : s ∈ mk t h₁ h₂ h₃s ∈ mk t h₁ h₂ h₃ ↔ s ∈ t :=
  Iff.rfl

Membership in Constructed Filter Equivalence

Informal description

For any collection of sets $t$ on a type $\alpha$ and any subset $s$ of $\alpha$, the statement $s$ belongs to the filter constructed from $t$ (with the necessary filter properties $h₁$, $h₂$, $h₃$) if and only if $s$ belongs to $t$.

Filter.mem_sets theorem

: s ∈ f.sets ↔ s ∈ f

Full source

@[simp]
protected theorem mem_sets : s ∈ f.setss ∈ f.sets ↔ s ∈ f :=
  Iff.rfl

Equivalence of Filter Membership and Set Collection Membership

Informal description

For any filter $f$ on a type $\alpha$ and any subset $s$ of $\alpha$, the statement $s$ belongs to the collection of sets defining $f$ if and only if $s$ belongs to $f$.

Filter.univ_mem theorem

: univ ∈ f

Full source

@[simp]
theorem univ_mem : univuniv ∈ f :=
  f.univ_sets

Universal Set Belongs to Every Filter

Informal description

For any filter $f$ on a type $\alpha$, the universal set $\text{univ} = \alpha$ belongs to $f$.

Filter.mem_of_superset theorem

{x y : Set α} (hx : x ∈ f) (hxy : x ⊆ y) : y ∈ f

Full source

theorem mem_of_superset {x y : Set α} (hx : x ∈ f) (hxy : x ⊆ y) : y ∈ f :=
  f.sets_of_superset hx hxy

Filter Upward Closure Property

Informal description

For any filter $f$ on a type $\alpha$ and any subsets $x, y \subseteq \alpha$, if $x \in f$ and $x \subseteq y$, then $y \in f$.

Filter.univ_mem' theorem

(h : ∀ a, a ∈ s) : s ∈ f

Full source

theorem univ_mem' (h : ∀ a, a ∈ s) : s ∈ f :=
  mem_of_superset univ_mem fun x _ => h x

Universal Membership in Filter via Total Containment

Informal description

For any filter $f$ on a type $\alpha$ and any subset $s \subseteq \alpha$, if every element $a \in \alpha$ belongs to $s$, then $s$ belongs to $f$.

Filter.inter_mem theorem

(hs : s ∈ f) (ht : t ∈ f) : s ∩ t ∈ f

Full source

theorem inter_mem (hs : s ∈ f) (ht : t ∈ f) : s ∩ ts ∩ t ∈ f :=
  f.inter_sets hs ht

Intersection of Filter Sets Belongs to Filter

Informal description

For any filter $f$ on a type $\alpha$ and any two sets $s, t \subseteq \alpha$, if $s$ belongs to $f$ and $t$ belongs to $f$, then their intersection $s \cap t$ also belongs to $f$.

Filter.mp_mem theorem

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

Full source

theorem mp_mem (hs : s ∈ f) (h : { x | x ∈ s → x ∈ t }{ x | x ∈ s → x ∈ t } ∈ f) : t ∈ f :=
  mem_of_superset (inter_mem hs h) fun _ ⟨h₁, h₂⟩ => h₂ h₁

Modus Ponens Property for Filters

Informal description

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

Filter.copy definition

(f : Filter α) (S : Set (Set α)) (hmem : ∀ s, s ∈ S ↔ s ∈ f) : Filter α

Full source

/-- Override `sets` field of a filter to provide better definitional equality. -/
protected def copy (f : Filter α) (S : Set (Set α)) (hmem : ∀ s, s ∈ Ss ∈ S ↔ s ∈ f) : Filter α where
  sets := S
  univ_sets := (hmem _).2 univ_mem
  sets_of_superset h hsub := (hmem _).2 <| mem_of_superset ((hmem _).1 h) hsub
  inter_sets h₁ h₂ := (hmem _).2 <| inter_mem ((hmem _).1 h₁) ((hmem _).1 h₂)

Copy of a filter with a specified collection of sets

Informal description

Given a filter $f$ on a type $\alpha$ and a collection of subsets $S$ of $\alpha$ such that $s \in S$ if and only if $s \in f$ for any subset $s$ of $\alpha$, the function `Filter.copy` constructs a new filter with $S$ as its underlying collection of sets. This new filter has the same properties as $f$: it contains the entire set $\alpha$, is closed under supersets, and is closed under finite intersections.

Filter.mem_copy theorem

{S hmem} : s ∈ f.copy S hmem ↔ s ∈ S

Full source

@[simp] theorem mem_copy {S hmem} : s ∈ f.copy S hmems ∈ f.copy S hmem ↔ s ∈ S := Iff.rfl

Membership in Filter Copy is Equivalent to Membership in Specified Set Collection

Informal description

For any filter $f$ on a type $\alpha$, any collection of subsets $S$ of $\alpha$, and any subset $s$ of $\alpha$, the subset $s$ belongs to the filter `f.copy S hmem` if and only if $s$ belongs to $S$, where `hmem` is a proof that $s \in S \leftrightarrow s \in f$ for all subsets $s$ of $\alpha$.

Filter.comk definition

 (p : Set α → Prop) (he : p ∅) (hmono : ∀ t, p t → ∀ s ⊆ t, p s) (hunion : ∀ s, p s → ∀ t, p t → p (s ∪ t)) : Filter α

Full source

/-- Construct a filter from a property that is stable under finite unions.
A set `s` belongs to `Filter.comk p _ _ _` iff its complement satisfies the predicate `p`.
This constructor is useful to define filters like `Filter.cofinite`. -/
def comk (p : Set α → Prop) (he : p ∅) (hmono : ∀ t, p t → ∀ s ⊆ t, p s)
    (hunion : ∀ s, p s → ∀ t, p t → p (s ∪ t)) : Filter α where
  sets := {t | p tᶜ}
  univ_sets := by simpa
  sets_of_superset := fun ht₁ ht => hmono _ ht₁ _ (compl_subset_compl.2 ht)
  inter_sets := fun ht₁ ht₂ => by simp [compl_inter, hunion _ ht₁ _ ht₂]

Filter generated by a predicate on complements

Informal description

Given a predicate $ p $ on subsets of a type $ \alpha $ that satisfies: 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), the filter `Filter.comk p he hmono hunion` is defined as the collection of all subsets $ s $ of $ \alpha $ whose complement $ s^c $ satisfies $ p $.

Filter.mem_comk theorem

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

Full source

@[simp]
lemma mem_comk {p : Set α → Prop} {he hmono hunion s} :
    s ∈ comk p he hmono hunions ∈ comk p he hmono hunion ↔ p sᶜ :=
  .rfl

Membership Criterion for Complement-Generated Filter

Informal description

For a 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$ belongs to the filter $\text{comk}\ p\ he\ hmono\ hunion$ if and only if the complement $s^c$ satisfies $p$.

Filter.principal definition

(s : Set α) : Filter α

Full source

/-- The principal filter of `s` is the collection of all supersets of `s`. -/
def principal (s : Set α) : Filter α where
  sets := { t | s ⊆ t }
  univ_sets := subset_univ s
  sets_of_superset hx := Subset.trans hx
  inter_sets := subset_inter

Principal filter generated by a set

Informal description

The principal filter generated by a set $s$ in a type $\alpha$ is the collection of all subsets of $\alpha$ that contain $s$. Formally, it is defined as the filter whose sets are $\{ t \mid s \subseteq t \}$.

Filter.term𝓟 definition

: Lean.ParserDescr✝

Full source

@[inherit_doc]
scoped notation "𝓟" => Filter.principal

Principal filter notation

Informal description

The notation `𝓟 s` represents the principal filter generated by the set `s`, which is the filter consisting of all supersets of `s`.

Filter.mem_principal theorem

: s ∈ 𝓟 t ↔ t ⊆ s

Full source

@[simp] theorem mem_principal : s ∈ 𝓟 ts ∈ 𝓟 t ↔ t ⊆ s := Iff.rfl

Membership in Principal Filter is Equivalent to Reverse Inclusion

Informal description

For any sets $s$ and $t$ in a type $\alpha$, the set $s$ belongs to the principal filter generated by $t$ (denoted $\mathcal{P}(t)$) if and only if $t$ is a subset of $s$, i.e., $s \in \mathcal{P}(t) \leftrightarrow t \subseteq s$.

Filter.instPure instance

: Pure Filter

Full source

/-- `pure x` is the set of sets that contain `x`. It is equal to `𝓟 {x}` but
with this definition we have `s ∈ pure a` defeq `a ∈ s`. -/
instance : Pure Filter where
  pure x := .copy (𝓟 {x}) {s | x ∈ s} fun _ ↦ by simp

The Pure Filter as Principal Filter of a Singleton

Informal description

For any type $\alpha$, the `pure` operation constructs a filter on $\alpha$ such that a set $s$ is in `pure x` if and only if $x \in s$. This is equivalent to the principal filter $\mathcal{P}\{x\}$ generated by the singleton set $\{x\}$, but defined in a way that makes the membership condition $s \in \text{pure } x$ definitionally equal to $x \in s$.

Filter.mem_pure theorem

{a : α} {s : Set α} : s ∈ (pure a : Filter α) ↔ a ∈ s

Full source

@[simp]
theorem mem_pure {a : α} {s : Set α} : s ∈ (pure a : Filter α)s ∈ (pure a : Filter α) ↔ a ∈ s :=
  Iff.rfl

Membership in Pure Filter: $s \in \text{pure } a \leftrightarrow a \in s$

Informal description

For any element $a$ of type $\alpha$ and any subset $s$ of $\alpha$, the set $s$ belongs to the pure filter generated by $a$ if and only if $a$ is an element of $s$.

Filter.ker definition

(f : Filter α) : Set α

Full source

/-- The *kernel* of a filter is the intersection of all its sets. -/
def ker (f : Filter α) : Set α := ⋂₀ f.sets

Kernel of a filter

Informal description

The kernel of a filter $f$ on a type $\alpha$ is the intersection of all sets in $f$, denoted $\bigcap_{s \in f} s$.

Filter.join definition

(f : Filter (Filter α)) : Filter α

Full source

/-- The join of a filter of filters is defined by the relation `s ∈ join f ↔ {t | s ∈ t} ∈ f`. -/
def join (f : Filter (Filter α)) : Filter α where
  sets := { s | { t : Filter α | s ∈ t } ∈ f }
  univ_sets := by simp only [mem_setOf_eq, univ_mem, setOf_true]
  sets_of_superset hx xy := mem_of_superset hx fun f h => mem_of_superset h xy
  inter_sets hx hy := mem_of_superset (inter_mem hx hy) fun f ⟨h₁, h₂⟩ => inter_mem h₁ h₂

Join of a filter of filters

Informal description

The join of a filter of filters $ f $ on a type $ \alpha $ is defined as the filter where a set $ s $ belongs to $ \text{join } f $ if and only if the collection of all filters $ t $ (on $ \alpha $) that contain $ s $ belongs to $ f $. In other words, $ s \in \text{join } f \leftrightarrow \{ t \mid s \in t \} \in f $.

Filter.mem_join theorem

{s : Set α} {f : Filter (Filter α)} : s ∈ join f ↔ {t | s ∈ t} ∈ f

Full source

@[simp]
theorem mem_join {s : Set α} {f : Filter (Filter α)} : s ∈ join fs ∈ join f ↔ { t | s ∈ t } ∈ f :=
  Iff.rfl

Characterization of Membership in Filter Join

Informal description

For any set $s$ in a type $\alpha$ and any filter $f$ on the space of filters on $\alpha$, the set $s$ belongs to the join of $f$ if and only if the collection of all filters containing $s$ belongs to $f$. In other words: $$ s \in \bigvee f \leftrightarrow \{ t \mid s \in t \} \in f. $$

Filter.instPartialOrder instance

: PartialOrder (Filter α)

Full source

instance : PartialOrder (Filter α) where
  le f g := ∀ ⦃U : Set α⦄, U ∈ g → U ∈ f
  le_antisymm a b h₁ h₂ := filter_eq <| Subset.antisymm h₂ h₁
  le_refl a := Subset.rfl
  le_trans a b c h₁ h₂ := Subset.trans h₂ h₁

Partial Order Structure on Filters

Informal description

The collection of filters on a type $\alpha$ forms a partial order under the inclusion relation $\subseteq$, where for two filters $F$ and $G$, $F \subseteq G$ if every set in $G$ is also in $F$.

Filter.le_def theorem

: f ≤ g ↔ ∀ x ∈ g, x ∈ f

Full source

theorem le_def : f ≤ g ↔ ∀ x ∈ g, x ∈ f :=
  Iff.rfl

Filter Inclusion Criterion: $f \leq g$ iff All Sets in $g$ Belong to $f$

Informal description

For two filters $f$ and $g$ on a type $\alpha$, the inequality $f \leq g$ holds if and only if every set $x$ that belongs to $g$ also belongs to $f$.

Filter.instSupSet instance

: SupSet (Filter α)

Full source

instance instSupSet : SupSet (Filter α) where
  sSup S := join (𝓟 S)

Complete Lattice Structure on Filters

Informal description

The collection of filters on a type $\alpha$ forms a complete lattice with respect to inclusion, where the supremum of a set of filters is the intersection of all filters in the set.

Filter.mem_sSup theorem

{S : Set (Filter α)} : s ∈ sSup S ↔ ∀ f ∈ S, s ∈ f

Full source

@[simp] theorem mem_sSup {S : Set (Filter α)} : s ∈ sSup Ss ∈ sSup S ↔ ∀ f ∈ S, s ∈ f := .rfl

Characterization of Membership in Filter Supremum: $s \in \bigvee S \leftrightarrow \forall f \in S, s \in f$

Informal description

For a set $S$ of filters on a type $\alpha$ and a subset $s \subseteq \alpha$, $s$ belongs to the supremum of $S$ (denoted $\bigvee S$) if and only if $s$ belongs to every filter $f$ in $S$.

Filter.sInf definition

(s : Set (Filter α)) : Filter α

Full source

/-- Infimum of a set of filters.
This definition is marked as irreducible
so that Lean doesn't try to unfold it when unifying expressions. -/
@[irreducible]
protected def sInf (s : Set (Filter α)) : Filter α := sSup (lowerBounds s)

Infimum of a set of filters

Informal description

The infimum of a set of filters $ s $ on a type $ \alpha $ is defined as the supremum of the set of all lower bounds of $ s $. In other words, it is the largest filter that is contained in every filter in $ s $.

Filter.instInfSet instance

: InfSet (Filter α)

Full source

instance instInfSet : InfSet (Filter α) where
  sInf := Filter.sInf

Infimum Structure on Filters

Informal description

The collection of filters on a type $\alpha$ has an infimum structure, where the infimum of a set of filters is the largest filter contained in every filter in the set.

Filter.sSup_lowerBounds theorem

(s : Set (Filter α)) : sSup (lowerBounds s) = sInf s

Full source

protected theorem sSup_lowerBounds (s : Set (Filter α)) : sSup (lowerBounds s) = sInf s := by
  simp [sInf, Filter.sInf]

Supremum of Lower Bounds Equals Infimum for Filters

Informal description

For any set $s$ of filters on a type $\alpha$, the supremum of the set of all lower bounds of $s$ is equal to the infimum of $s$. In other words, $\bigvee (\text{lowerBounds } s) = \bigwedge s$.

Filter.instTop instance

: Top (Filter α)

Full source

instance : Top (Filter α) where
  top := .copy (sSup (Set.range pure)) {s | ∀ x, x ∈ s} <| by simp

The Top Filter as the Collection of All Subsets

Informal description

The collection of all filters on a type $\alpha$ has a top element, which is the filter containing every subset of $\alpha$.

Filter.mem_top_iff_forall theorem

{s : Set α} : s ∈ (⊤ : Filter α) ↔ ∀ x, x ∈ s

Full source

theorem mem_top_iff_forall {s : Set α} : s ∈ (⊤ : Filter α)s ∈ (⊤ : Filter α) ↔ ∀ x, x ∈ s :=
  Iff.rfl

Characterization of Membership in the Top Filter: $s \in \top \leftrightarrow \forall x, x \in s$

Informal description

For any subset $s$ of a type $\alpha$, $s$ belongs to the top filter $\top$ on $\alpha$ if and only if every element $x$ of $\alpha$ is in $s$.

Filter.mem_top theorem

{s : Set α} : s ∈ (⊤ : Filter α) ↔ s = univ

Full source

@[simp]
theorem mem_top {s : Set α} : s ∈ (⊤ : Filter α)s ∈ (⊤ : Filter α) ↔ s = univ := by
  rw [mem_top_iff_forall, eq_univ_iff_forall]

Characterization of Membership in the Top Filter: $s \in \top \leftrightarrow s = \text{univ}$

Informal description

For any subset $s$ of a type $\alpha$, $s$ belongs to the top filter $\top$ on $\alpha$ if and only if $s$ is equal to the universal set $\text{univ}$ (the set containing all elements of $\alpha$).

Filter.instBot instance

: Bot (Filter α)

Full source

instance : Bot (Filter α) where
  bot := .copy (sSup ∅) univ <| by simp

Bottom Filter in the Lattice of Filters

Informal description

The collection of filters on any type $\alpha$ has a bottom element $\bot$, which is the filter containing all subsets of $\alpha$.

Filter.mem_bot theorem

{s : Set α} : s ∈ (⊥ : Filter α)

Full source

@[simp]
theorem mem_bot {s : Set α} : s ∈ (⊥ : Filter α) :=
  trivial

Every Set Belongs to the Bottom Filter

Informal description

For any set $s$ of type $\alpha$, $s$ belongs to the bottom filter $\bot$ on $\alpha$.

Filter.instInf instance

: Min (Filter α)

Full source

/-- The infimum of filters is the filter generated by intersections
  of elements of the two filters. -/
instance instInf : Min (Filter α) :=
  ⟨fun f g : Filter α =>
    { sets := { s | ∃ a ∈ f, ∃ b ∈ g, s = a ∩ b }
      univ_sets := ⟨_, univ_mem, _, univ_mem, by simp⟩
      sets_of_superset := by
        rintro x y ⟨a, ha, b, hb, rfl⟩ xy
        refine ⟨a ∪ y, mem_of_superset ha subset_union_left, b ∪ y,
          mem_of_superset hb subset_union_left, ?_⟩
        rw [← inter_union_distrib_right, union_eq_self_of_subset_left xy]
      inter_sets := by
        rintro x y ⟨a, ha, b, hb, rfl⟩ ⟨c, hc, d, hd, rfl⟩
        refine ⟨a ∩ c, inter_mem ha hc, b ∩ d, inter_mem hb hd, ?_⟩
        ac_rfl }⟩

Infimum of Filters as Intersection-Generated Filter

Informal description

The infimum of two filters $F$ and $G$ on a type $\alpha$ is the filter generated by all intersections $U \cap V$ where $U \in F$ and $V \in G$.

Filter.instSup instance

: Max (Filter α)

Full source

/-- The supremum of two filters is the filter that contains sets that belong to both filters. -/
instance instSup : Max (Filter α) where
  max f g := .copy (sSup {f, g}) {s | s ∈ f ∧ s ∈ g} <| by simp

Supremum of Two Filters as Their Common Subsets

Informal description

The supremum of two filters $F$ and $G$ on a type $\alpha$ is the filter consisting of all subsets $s$ of $\alpha$ such that $s$ belongs to both $F$ and $G$.

Filter.NeBot structure

(f : Filter α)

Full source

/-- A filter is `NeBot` if it is not equal to `⊥`, or equivalently the empty set does not belong to
the filter. Bourbaki include this assumption in the definition of a filter but we prefer to have a
`CompleteLattice` structure on `Filter _`, so we use a typeclass argument in lemmas instead. -/
class NeBot (f : Filter α) : Prop where
  /-- The filter is nontrivial: `f ≠ ⊥` or equivalently, `∅ ∉ f`. -/
  ne' : f ≠ ⊥

Non-trivial filter

Informal description

A filter `f` on a type `α` is called *non-trivial* (or *NeBot*) if it is not equal to the bottom filter `⊥`, or equivalently, if the empty set does not belong to the filter. This condition is often required in lemmas and definitions to ensure meaningful results.

Filter.neBot_iff theorem

{f : Filter α} : NeBot f ↔ f ≠ ⊥

Full source

theorem neBot_iff {f : Filter α} : NeBotNeBot f ↔ f ≠ ⊥ :=
  ⟨fun h => h.1, fun h => ⟨h⟩⟩

Non-trivial Filter Characterization: $f \neq \bot$

Informal description

A filter $f$ on a type $\alpha$ is non-trivial if and only if it is not equal to the bottom filter $\bot$.

Filter.Eventually definition

(p : α → Prop) (f : Filter α) : Prop

Full source

/-- `f.Eventually p` or `∀ᶠ x in f, p x` mean that `{x | p x} ∈ f`. E.g., `∀ᶠ x in atTop, p x`
means that `p` holds true for sufficiently large `x`. -/
protected def Eventually (p : α → Prop) (f : Filter α) : Prop :=
  { x | p x }{ x | p x } ∈ f

"Eventually" property with respect to a filter

Informal description

Given a filter $f$ on a type $\alpha$ and a predicate $p : \alpha \to \text{Prop}$, the expression $f.\text{Eventually}\, p$ (or equivalently $\forallᶠ x \text{ in } f, p x$) means that the set $\{x \mid p x\}$ belongs to the filter $f$. This indicates that the property $p$ holds for all elements in some set that is in the filter $f$, i.e., $p$ holds "eventually" with respect to $f$. For example, $\forallᶠ x \text{ in } \text{atTop}, p x$ means that $p$ holds for all sufficiently large $x$.

Filter.term∀ᶠ_In_,_ definition

: Lean.ParserDescr✝

Full source

@[inherit_doc Filter.Eventually]
notation3 "∀ᶠ "(...)" in "f", "r:(scoped p => Filter.Eventually p f) => r

"Eventually all" notation for filters

Informal description

The notation `∀ᶠ x in f, p x` represents the statement that the set `{x | p x}` belongs to the filter `f`, meaning the property `p` holds for all `x` in some set that is in the filter `f`. This is read as "for eventually all `x` in `f`, `p x` holds".

Filter.term∀ᶠ_In_,_.delab_app.Filter.Eventually definition

: Delab✝

Full source

@[inherit_doc Filter.Eventually]
notation3 "∀ᶠ "(...)" in "f", "r:(scoped p => Filter.Eventually p f) => r

"Eventually all" notation for filters

Informal description

The notation `∀ᶠ x in f, p x` represents the statement that the property `p` holds for all `x` in some set belonging to the filter `f`. This is read as "for eventually all `x` in `f`, `p x` holds".

Filter.Frequently definition

(p : α → Prop) (f : Filter α) : Prop

Full source

/-- `f.Frequently p` or `∃ᶠ x in f, p x` mean that `{x | ¬p x} ∉ f`. E.g., `∃ᶠ x in atTop, p x`
means that there exist arbitrarily large `x` for which `p` holds true. -/
protected def Frequently (p : α → Prop) (f : Filter α) : Prop :=
  ¬∀ᶠ x in f, ¬p x

Frequently occurring property with respect to a filter

Informal description

Given a filter $f$ on a type $\alpha$ and a predicate $p : \alpha \to \text{Prop}$, the expression $f.\text{Frequently}\, p$ (or equivalently $\existsᶠ x \text{ in } f, p x$) means that the set $\{x \mid \neg p x\}$ does not belong to the filter $f$. This indicates that the property $p$ holds for some elements in every set of the filter $f$, i.e., $p$ holds "frequently" with respect to $f$. For example, $\existsᶠ x \text{ in } \text{atTop}, p x$ means that $p$ holds for arbitrarily large $x$.

Filter.term∃ᶠ_In_,_ definition

: Lean.ParserDescr✝

Full source

@[inherit_doc Filter.Frequently]
notation3 "∃ᶠ "(...)" in "f", "r:(scoped p => Filter.Frequently p f) => r

Frequently notation for filters

Informal description

The notation `∃ᶠ x in f, p x` represents the statement that the set `{x | p x}` is frequently in the filter `f`, meaning that the complement of `{x | p x}` is not in `f`. In other words, the property `p` holds for some elements in every set of the filter `f`.

Filter.term∃ᶠ_In_,_.delab_app.Filter.Frequently definition

: Delab✝

Full source

@[inherit_doc Filter.Frequently]
notation3 "∃ᶠ "(...)" in "f", "r:(scoped p => Filter.Frequently p f) => r

Frequently notation for filters

Informal description

The notation `∃ᶠ x in f, p x` represents the statement that the property `p` holds frequently in the filter `f`, meaning that the set `{x | ¬p x}` does not belong to `f`. In other words, for every set in the filter `f`, there exists some element in that set where `p` holds.

Filter.EventuallyEq definition

(l : Filter α) (f g : α → β) : Prop

Full source

/-- Two functions `f` and `g` are *eventually equal* along a filter `l` if the set of `x` such that
`f x = g x` belongs to `l`. -/
def EventuallyEq (l : Filter α) (f g : α → β) : Prop :=
  ∀ᶠ x in l, f x = g x

Eventually equal functions with respect to a filter

Informal description

Two functions $f$ and $g$ from $\alpha$ to $\beta$ are *eventually equal* with respect to a filter $l$ on $\alpha$ if the set of points $x$ where $f(x) = g(x)$ belongs to $l$. In other words, $f$ and $g$ agree on some set in the filter $l$.

Filter.term_=ᶠ[_]_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
notation:50 f " =ᶠ[" l:50 "] " g:50 => EventuallyEq l f g

Eventually equal functions with respect to a filter

Informal description

The notation $f =ᶠ[l] g$ means that the functions $f$ and $g$ are eventually equal with respect to the filter $l$, i.e., the set $\{x | f(x) = g(x)\}$ belongs to the filter $l$.

Filter.EventuallyLE definition

[LE β] (l : Filter α) (f g : α → β) : Prop

Full source

/-- A function `f` is eventually less than or equal to a function `g` at a filter `l`. -/
def EventuallyLE [LE β] (l : Filter α) (f g : α → β) : Prop :=
  ∀ᶠ x in l, f x ≤ g x

Eventually less than or equal to with respect to a filter

Informal description

Given a type $\beta$ with a less-than-or-equal relation $\leq$, a filter $l$ on a type $\alpha$, and two functions $f, g : \alpha \to \beta$, the relation $f \leqᶠ[l] g$ holds if the set $\{x \mid f(x) \leq g(x)\}$ belongs to the filter $l$. This means that $f(x) \leq g(x)$ holds for all $x$ in some set that is in the filter $l$, i.e., $f$ is eventually less than or equal to $g$ with respect to $l$.

Filter.term_≤ᶠ[_]_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
notation:50 f " ≤ᶠ[" l:50 "] " g:50 => EventuallyLE l f g

Eventually less than or equal to with respect to a filter

Informal description

The notation $f \leqᶠ[l] g$ represents the statement that $f(x) \leq g(x)$ holds eventually with respect to the filter $l$, meaning the set $\{x | f(x) \leq g(x)\}$ belongs to the filter $l$.

Filter.map definition

(m : α → β) (f : Filter α) : Filter β

Full source

/-- The forward map of a filter -/
def map (m : α → β) (f : Filter α) : Filter β where
  sets := preimagepreimage m ⁻¹' f.sets
  univ_sets := univ_mem
  sets_of_superset hs st := mem_of_superset hs fun _x hx ↦ st hx
  inter_sets hs ht := inter_mem hs ht

Image filter under a function

Informal description

Given a function $ m : \alpha \to \beta $ and a filter $ f $ on $ \alpha $, the filter $ \text{Filter.map } m f $ on $ \beta $ is defined as the collection of all subsets $ s \subseteq \beta $ whose preimage $ m^{-1}(s) $ belongs to $ f $. This operation preserves the filter properties: 1. The entire set $ \beta $ is in the mapped filter since $ m^{-1}(\beta) = \alpha \in f $. 2. If $ s \in \text{Filter.map } m f $ and $ s \subseteq t $, then $ t \in \text{Filter.map } m f $ because $ m^{-1}(s) \subseteq m^{-1}(t) $ and $ f $ is upwards-closed. 3. If $ s, t \in \text{Filter.map } m f $, then $ s \cap t \in \text{Filter.map } m f $ because $ m^{-1}(s \cap t) = m^{-1}(s) \cap m^{-1}(t) \in f $.

Filter.Tendsto definition

(f : α → β) (l₁ : Filter α) (l₂ : Filter β)

Full source

/-- `Filter.Tendsto` is the generic "limit of a function" predicate.
  `Tendsto f l₁ l₂` asserts that for every `l₂` neighborhood `a`,
  the `f`-preimage of `a` is an `l₁` neighborhood. -/
def Tendsto (f : α → β) (l₁ : Filter α) (l₂ : Filter β) :=
  l₁.map f ≤ l₂

Limit of a function with respect to filters

Informal description

Given a function $ f : \alpha \to \beta $ and filters $ l_1 $ on $ \alpha $ and $ l_2 $ on $ \beta $, the predicate $ \text{Tendsto } f l_1 l_2 $ asserts that for every set $ s $ in the filter $ l_2 $, the preimage $ f^{-1}(s) $ belongs to the filter $ l_1 $. In other words, $ f $ maps $ l_1 $-large sets to $ l_2 $-large sets.

Filter.comap definition

(m : α → β) (f : Filter β) : Filter α

Full source

/-- The inverse map of a filter. A set `s` belongs to `Filter.comap m f` if either of the following
equivalent conditions hold.

1. There exists a set `t ∈ f` such that `m ⁻¹' t ⊆ s`. This is used as a definition.
2. The set `kernImage m s = {y | ∀ x, m x = y → x ∈ s}` belongs to `f`, see `Filter.mem_comap'`.
3. The set `(m '' sᶜ)ᶜ` belongs to `f`, see `Filter.mem_comap_iff_compl` and
`Filter.compl_mem_comap`. -/
def comap (m : α → β) (f : Filter β) : Filter α where
  sets := { s | ∃ t ∈ f, m ⁻¹' t ⊆ s }
  univ_sets := ⟨univ, univ_mem, subset_univ _⟩
  sets_of_superset := fun ⟨a', ha', ma'a⟩ ab => ⟨a', ha', ma'a.trans ab⟩
  inter_sets := fun ⟨a', ha₁, ha₂⟩ ⟨b', hb₁, hb₂⟩ =>
    ⟨a' ∩ b', inter_mem ha₁ hb₁, inter_subset_inter ha₂ hb₂⟩

Preimage filter under a function

Informal description

Given a function $ m : \alpha \to \beta $ and a filter $ f $ on $ \beta $, the *comap filter* $ \text{Filter.comap } m f $ is the filter on $ \alpha $ consisting of all subsets $ s \subseteq \alpha $ for which there exists a set $ t \in f $ such that the preimage $ m^{-1}(t) $ is contained in $ s $. Equivalently, a set $ s $ belongs to $ \text{Filter.comap } m f $ if the *kernel image* $ \{ y \mid \forall x, m(x) = y \to x \in s \} $ belongs to $ f $, or if the complement of the image of the complement of $ s $ belongs to $ f $.

Filter.coprod definition

(f : Filter α) (g : Filter β) : Filter (α × β)

Full source

/-- Coproduct of filters. -/
protected def coprod (f : Filter α) (g : Filter β) : Filter (α × β) :=
  f.comap Prod.fst ⊔ g.comap Prod.snd

Coproduct filter

Informal description

The coproduct filter of two filters $ f $ on type $ \alpha $ and $ g $ on type $ \beta $ is the filter on $ \alpha \times \beta $ generated by the supremum of the preimage filters of $ f $ under the first projection $ \text{Prod.fst} $ and the preimage filter of $ g $ under the second projection $ \text{Prod.snd} $. In other words, it is the smallest filter containing all sets of the form $ A \times \beta $ for $ A \in f $ and $ \alpha \times B $ for $ B \in g $.

Filter.instSProd instance

: SProd (Filter α) (Filter β) (Filter (α × β))

Full source

/-- Product of filters. This is the filter generated by cartesian products
of elements of the component filters. -/
instance instSProd : SProd (Filter α) (Filter β) (Filter (α × β)) where
  sprod f g := f.comap Prod.fst ⊓ g.comap Prod.snd

Product Filter Construction via Cartesian Products

Informal description

For any two filters $F$ on type $\alpha$ and $G$ on type $\beta$, the product filter $F \timesˢ G$ is defined as the filter on $\alpha \times \beta$ generated by all Cartesian products $U \times V$ where $U \in F$ and $V \in G$. This operation satisfies the properties of a set product, making it compatible with the filter structure.

Filter.prod definition

(f : Filter α) (g : Filter β) : Filter (α × β)

Full source

/-- Product of filters. This is the filter generated by cartesian products
of elements of the component filters.
Deprecated. Use `f ×ˢ g` instead. -/
@[deprecated " Use `f ×ˢ g` instead." (since := "2024-11-29")]
protected def prod (f : Filter α) (g : Filter β) : Filter (α × β) := f ×ˢ g

Product filter of two filters

Informal description

The product filter of two filters $f$ on type $\alpha$ and $g$ on type $\beta$ is the filter on $\alpha \times \beta$ generated by all Cartesian products $U \times V$ where $U \in f$ and $V \in g$. This construction is equivalent to $f \timesˢ g$.

Filter.prod_eq_inf theorem

(f : Filter α) (g : Filter β) : f ×ˢ g = f.comap Prod.fst ⊓ g.comap Prod.snd

Full source

theorem prod_eq_inf (f : Filter α) (g : Filter β) : f ×ˢ g = f.comap Prod.fst ⊓ g.comap Prod.snd :=
  rfl

Product Filter as Infimum of Preimage Filters

Informal description

For any filters $f$ on a type $\alpha$ and $g$ on a type $\beta$, the product filter $f \times^s g$ on $\alpha \times \beta$ is equal to the infimum of the preimage filters $f \circ \pi_1$ and $g \circ \pi_2$, where $\pi_1$ and $\pi_2$ are the first and second projection maps from $\alpha \times \beta$ to $\alpha$ and $\beta$ respectively. In other words, $f \times^s g = \text{comap } \pi_1 f \sqcap \text{comap } \pi_2 g$.

Filter.pi definition

{ι : Type*} {α : ι → Type*} (f : ∀ i, Filter (α i)) : Filter (∀ i, α i)

Full source

/-- The product of an indexed family of filters. -/
def pi {ι : Type*} {α : ι → Type*} (f : ∀ i, Filter (α i)) : Filter (∀ i, α i) :=
  ⨅ i, comap (Function.eval i) (f i)

Pi filter of an indexed family of filters

Informal description

Given an indexed family of types $\alpha_i$ and a corresponding family of filters $f_i$ on each $\alpha_i$, the *pi filter* $\text{Filter.pi } f$ is the filter on the product type $\forall i, \alpha_i$ defined as the infimum of the preimage filters $\text{comap } (\text{eval } i) (f_i)$ for each index $i$, where $\text{eval } i$ denotes the evaluation function at index $i$. In other words, a set $s$ belongs to $\text{Filter.pi } f$ if and only if for every index $i$, there exists a set $t_i \in f_i$ such that the evaluation of any function in $s$ at $i$ lies in $t_i$.

Filter.bind definition

(f : Filter α) (m : α → Filter β) : Filter β

Full source

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

Unfortunately, this `bind` does not result in the expected applicative. See `Filter.seq` for the
applicative instance. -/
def bind (f : Filter α) (m : α → Filter β) : Filter β :=
  join (map m f)

Monadic bind operation on filters

Informal description

Given a filter $ f $ on a type $ \alpha $ and a function $ m : \alpha \to \text{Filter } \beta $, the bind operation $ \text{Filter.bind } f m $ constructs a filter on $ \beta $ by first mapping each element $ x \in \alpha $ to its corresponding filter $ m(x) $ (resulting in a filter of filters on $ \beta $), and then taking the join of this filter of filters. More precisely, a set $ s \subseteq \beta $ belongs to $ \text{Filter.bind } f m $ if and only if the set of all $ x \in \alpha $ for which $ s \in m(x) $ belongs to $ f $. This operation is analogous to the monadic bind in functional programming, where the filter $ f $ is "bound" to the function $ m $ to produce a new filter on $ \beta $.

Filter.seq definition

(f : Filter (α → β)) (g : Filter α) : Filter β

Full source

/-- The applicative sequentiation operation. This is not induced by the bind operation. -/
def seq (f : Filter (α → β)) (g : Filter α) : Filter β where
  sets := { s | ∃ u ∈ f, ∃ t ∈ g, ∀ m ∈ u, ∀ x ∈ t, (m : α → β) x ∈ s }
  univ_sets := ⟨univ, univ_mem, univ, univ_mem, fun _ _ _ _ => trivial⟩
  sets_of_superset := fun ⟨t₀, t₁, h₀, h₁, h⟩ hst =>
    ⟨t₀, t₁, h₀, h₁, fun _ hx _ hy => hst <| h _ hx _ hy⟩
  inter_sets := fun ⟨t₀, ht₀, t₁, ht₁, ht⟩ ⟨u₀, hu₀, u₁, hu₁, hu⟩ =>
    ⟨t₀ ∩ u₀, inter_mem ht₀ hu₀, t₁ ∩ u₁, inter_mem ht₁ hu₁, fun _ ⟨hx₀, hx₁⟩ _ ⟨hy₀, hy₁⟩ =>
      ⟨ht _ hx₀ _ hy₀, hu _ hx₁ _ hy₁⟩⟩

Sequential composition of filters

Informal description

Given a filter `f` of functions from `α` to `β` and a filter `g` on `α`, the filter `Filter.seq f g` is defined as the collection of all subsets `s` of `β` for which there exist sets `u ∈ f` and `t ∈ g` such that for every function `m ∈ u` and every element `x ∈ t`, the application `m x` belongs to `s`. This operation combines two filters to form a new filter on `β` by considering all possible applications of functions from `f` to elements from `g`.

Filter.curry definition

(f : Filter α) (g : Filter β) : Filter (α × β)

Full source

/-- This filter is characterized by `Filter.eventually_curry_iff`:
`(∀ᶠ (x : α × β) in f.curry g, p x) ↔ ∀ᶠ (x : α) in f, ∀ᶠ (y : β) in g, p (x, y)`. Useful
in adding quantifiers to the middle of `Tendsto`s. See
`hasFDerivAt_of_tendstoUniformlyOnFilter`. -/
def curry (f : Filter α) (g : Filter β) : Filter (α × β) :=
  bind f fun a ↦ map (a, ·) g

Curried filter product

Informal description

Given filters $ f $ on $ \alpha $ and $ g $ on $ \beta $, the filter $ \text{Filter.curry } f g $ on $ \alpha \times \beta $ is characterized by the property that a set $ s \subseteq \alpha \times \beta $ belongs to $ \text{Filter.curry } f g $ if and only if for every $ x \in \alpha $, the set $ \{ y \in \beta \mid (x, y) \in s \} $ belongs to $ g $, and the set of all such $ x $ belongs to $ f $. More formally, $ \forall s \subseteq \alpha \times \beta $, \[ s \in \text{Filter.curry } f g \leftrightarrow \left( \forall x \in \alpha, \{ y \in \beta \mid (x, y) \in s \} \in g \right) \text{ and } \{ x \in \alpha \mid \{ y \in \beta \mid (x, y) \in s \} \in g \} \in f. \] This construction is useful for adding quantifiers in the middle of limits (e.g., in `Tendsto` statements).

Filter.instBind instance

: Bind Filter

Full source

instance : Bind Filter :=
  ⟨@Filter.bind⟩

Monad Structure on Filters via Bind Operation

Informal description

The type of filters on any type $\alpha$ forms a monad, where the bind operation is given by the filter bind operation. Specifically, for a filter $f$ on $\alpha$ and a function $m : \alpha \to \text{Filter } \beta$, the bind operation constructs a new filter on $\beta$ by combining the filters obtained from applying $m$ to elements in the sets of $f$.

Filter.instFunctor instance

: Functor Filter

Full source

instance : Functor Filter where map := @Filter.map

Functorial Structure of Filters

Informal description

The type of filters on any type $\alpha$ forms a functor, where the map operation is given by the preimage operation on filters.

Filter.lift definition

(f : Filter α) (g : Set α → Filter β)

Full source

/-- A variant on `bind` using a function `g` taking a set instead of a member of `α`.
This is essentially a push-forward along a function mapping each set to a filter. -/
protected def lift (f : Filter α) (g : Set α → Filter β) :=
  ⨅ s ∈ f, g s

Filter lift operation via set-valued function

Informal description

Given a filter $f$ on a type $\alpha$ and a function $g$ that maps subsets of $\alpha$ to filters on a type $\beta$, the operation $\text{lift}$ constructs a new filter on $\beta$ by taking the infimum of the filters $g(s)$ for all sets $s$ in $f$. In other words, $\text{lift}\, f\, g$ is the largest filter on $\beta$ that is contained in every $g(s)$ for $s \in f$.

Filter.lift' definition

(f : Filter α) (h : Set α → Set β)

Full source

/-- Specialize `lift` to functions `Set α → Set β`. This can be viewed as a generalization of `map`.
This is essentially a push-forward along a function mapping each set to a set. -/
protected def lift' (f : Filter α) (h : Set α → Set β) :=
  f.lift (𝓟𝓟 ∘ h)

Filter lift via set-valued function

Informal description

Given a filter $f$ on a type $\alpha$ and a function $h$ that maps subsets of $\alpha$ to subsets of $\beta$, the operation $\text{lift'}$ constructs a new filter on $\beta$ by taking the principal filter generated by $h(s)$ for each set $s$ in $f$, and then forming the infimum of these principal filters. In other words, $\text{lift'}\, f\, h$ is the largest filter on $\beta$ that contains all the sets $h(s)$ for $s \in f$.

Filter.IsBounded definition

(r : α → α → Prop) (f : Filter α)

Full source

/-- `f.IsBounded r`: the filter `f` is eventually bounded w.r.t. the relation `r`,
i.e. eventually, it is bounded by some uniform bound.
`r` will be usually instantiated with `(· ≤ ·)` or `(· ≥ ·)`. -/
def IsBounded (r : α → α → Prop) (f : Filter α) :=
  ∃ b, ∀ᶠ x in f, r x b

Bounded filter with respect to a relation

Informal description

A filter $f$ on a type $\alpha$ is said to be *bounded* with respect to a relation $r : \alpha \to \alpha \to \text{Prop}$ if there exists some element $b \in \alpha$ such that for all $x$ in some set belonging to $f$, the relation $r(x, b)$ holds. In other words, the filter $f$ is eventually bounded by $b$ with respect to $r$. This is typically used when $r$ is an order relation like $\leq$ or $\geq$, indicating that the filter's elements are eventually uniformly bounded above or below by $b$.

Filter.IsBoundedUnder definition

(r : α → α → Prop) (f : Filter β) (u : β → α)

Full source

/-- `f.IsBoundedUnder (≺) u`: the image of the filter `f` under `u` is eventually bounded w.r.t.
the relation `≺`, i.e. eventually, it is bounded by some uniform bound. -/
def IsBoundedUnder (r : α → α → Prop) (f : Filter β) (u : β → α) :=
  (map u f).IsBounded r

Boundedness under a relation with respect to a function

Informal description

Given a relation $ r $ on a type $ \alpha $, a filter $ f $ on a type $ \beta $, and a function $ u : \beta \to \alpha $, the filter $ f $ is said to be *bounded under $ r $ with respect to $ u $* if the image filter $ \text{map } u f $ is bounded with respect to $ r $. This means there exists some element $ b \in \alpha $ such that for all $ y $ in some set belonging to $ f $, the relation $ r(u(y), b) $ holds. In other words, the values of $ u $ under the filter $ f $ are eventually bounded by $ b $ with respect to the relation $ r $.

Filter.IsCobounded definition

(r : α → α → Prop) (f : Filter α)

Full source

/-- `IsCobounded (≺) f` states that the filter `f` does not tend to infinity w.r.t. `≺`. This is
also called frequently bounded. Will be usually instantiated with `≤` or `≥`.

There is a subtlety in this definition: we want `f.IsCobounded` to hold for any `f` in the case of
complete lattices. This will be relevant to deduce theorems on complete lattices from their
versions on conditionally complete lattices with additional assumptions. We have to be careful in
the edge case of the trivial filter containing the empty set: the other natural definition
  `¬ ∀ a, ∀ᶠ n in f, a ≤ n`
would not work as well in this case.
-/
def IsCobounded (r : α → α → Prop) (f : Filter α) :=
  ∃ b, ∀ a, (∀ᶠ x in f, r x a) → r b a

Cobounded filter with respect to a relation

Informal description

A filter $f$ on a type $\alpha$ is called *cobounded* with respect to a relation $r : \alpha \to \alpha \to \text{Prop}$ if there exists a bound $b \in \alpha$ such that for any $a \in \alpha$, whenever the set $\{x \mid r(x, a)\}$ belongs to $f$, then $r(b, a)$ holds. This means that the filter $f$ does not tend to infinity with respect to $r$, i.e., it is frequently bounded.

Filter.IsCoboundedUnder definition

(r : α → α → Prop) (f : Filter β) (u : β → α)

Full source

/-- `IsCoboundedUnder (≺) f u` states that the image of the filter `f` under the map `u` does not
tend to infinity w.r.t. `≺`. This is also called frequently bounded. Will be usually instantiated
with `≤` or `≥`. -/
def IsCoboundedUnder (r : α → α → Prop) (f : Filter β) (u : β → α) :=
  (map u f).IsCobounded r

Cobounded filter under a function with respect to a relation

Informal description

Given a relation $ r : \alpha \to \alpha \to \text{Prop} $, a filter $ f $ on a type $ \beta $, and a function $ u : \beta \to \alpha $, the filter $ f $ is called *cobounded under $ u $ with respect to $ r $* if the image filter $ \text{Filter.map } u f $ is cobounded with respect to $ r $. This means that the filter $ f $ does not tend to infinity under the mapping $ u $ with respect to the relation $ r $, i.e., it is frequently bounded under $ u $.

Mathlib.Tactic.filterUpwards definition

: Lean.ParserDescr✝

Full source

/--
`filter_upwards [h₁, ⋯, hₙ]` replaces a goal of the form `s ∈ f` and terms
`h₁ : t₁ ∈ f, ⋯, hₙ : tₙ ∈ f` with `∀ x, x ∈ t₁ → ⋯ → x ∈ tₙ → x ∈ s`.
The list is an optional parameter, `[]` being its default value.

`filter_upwards [h₁, ⋯, hₙ] with a₁ a₂ ⋯ aₖ` is a short form for
`{ filter_upwards [h₁, ⋯, hₙ], intros a₁ a₂ ⋯ aₖ }`.

`filter_upwards [h₁, ⋯, hₙ] using e` is a short form for
`{ filter_upwards [h1, ⋯, hn], exact e }`.

Combining both shortcuts is done by writing `filter_upwards [h₁, ⋯, hₙ] with a₁ a₂ ⋯ aₖ using e`.
Note that in this case, the `aᵢ` terms can be used in `e`.
-/
syntax (name := filterUpwards) "filter_upwards" (" [" term,* "]")?
  (" with" (ppSpace colGt term:max)*)? (" using " term)? : tactic

`filter_upwards` tactic for filter goals

Informal description

The tactic `filter_upwards` transforms a goal of the form `s ∈ f` (asserting that the set `s` belongs to the filter `f`) into a universally quantified statement. Given hypotheses `h₁ : t₁ ∈ f, ..., hₙ : tₙ ∈ f`, it replaces the goal with `∀ x, x ∈ t₁ → ⋯ → x ∈ tₙ → x ∈ s`. Optional parameters allow for further refinement: - `filter_upwards [h₁, ..., hₙ] with a₁ ... aₖ` introduces variables `a₁, ..., aₖ` after applying the tactic. - `filter_upwards [h₁, ..., hₙ] using e` applies the term `e` to the transformed goal. - These can be combined as `filter_upwards [h₁, ..., hₙ] with a₁ ... aₖ using e`, where the variables `aᵢ` may be used in `e`.

Mathlib.Order.Filter.Defs

Main definitions

Notations

Implementation Notes

References