Mathlib.Order.Filter.AtTopBot.Defs

Filter.atTop definition

[Preorder α] : Filter α

Full source

/-- `atTop` is the filter representing the limit `→ ∞` on an ordered set.
  It is generated by the collection of up-sets `{b | a ≤ b}`.
  (The preorder need not have a top element for this to be well defined,
  and indeed is trivial when a top element exists.) -/
def atTop [Preorder α] : Filter α :=
  ⨅ a, 𝓟 (Ici a)

Filter at positive infinity (`atTop`)

Informal description

The filter `atTop` on a preorder $\alpha$ represents the limit tending to positive infinity. It is generated by the collection of all left-closed right-infinite intervals $[a, \infty)$ for $a \in \alpha$. This filter is well-defined even when the preorder does not have a top element.

Filter.atBot definition

[Preorder α] : Filter α

Full source

/-- `atBot` is the filter representing the limit `→ -∞` on an ordered set.
  It is generated by the collection of down-sets `{b | b ≤ a}`.
  (The preorder need not have a bottom element for this to be well defined,
  and indeed is trivial when a bottom element exists.) -/
def atBot [Preorder α] : Filter α :=
  ⨅ a, 𝓟 (Iic a)

Filter at negative infinity (`atBot`)

Informal description

The filter `atBot` on a preorder `α` represents the limit tending to negative infinity. It is generated by the collection of all left-infinite right-closed intervals $ (-\infty, a] $ for $ a \in \alpha $. This filter is well-defined even when the preorder does not have a bottom element.

Filter.mem_atTop theorem

[Preorder α] (a : α) : {b : α | a ≤ b} ∈ @atTop α _

Full source

theorem mem_atTop [Preorder α] (a : α) : { b : α | a ≤ b }{ b : α | a ≤ b } ∈ @atTop α _ :=
  mem_iInf_of_mem a <| Subset.refl _

Membership of Upper Set in `atTop` Filter

Informal description

For any element $a$ in a preorder $\alpha$, the set $\{b \in \alpha \mid a \leq b\}$ belongs to the filter `atTop` on $\alpha$.

Filter.Ici_mem_atTop theorem

[Preorder α] (a : α) : Ici a ∈ (atTop : Filter α)

Full source

theorem Ici_mem_atTop [Preorder α] (a : α) : IciIci a ∈ (atTop : Filter α) :=
  mem_atTop a

Membership of $[a, \infty)$ in the `atTop` filter

Informal description

For any element $a$ in a preorder $\alpha$, the left-closed right-infinite interval $[a, \infty)$ belongs to the filter `atTop` on $\alpha$.

Filter.Ioi_mem_atTop theorem

[Preorder α] [NoTopOrder α] (x : α) : Ioi x ∈ (atTop : Filter α)

Full source

theorem Ioi_mem_atTop [Preorder α] [NoTopOrder α] (x : α) : IoiIoi x ∈ (atTop : Filter α) :=
  let ⟨z, hz⟩ := exists_not_le x
  mem_of_superset (inter_mem (mem_atTop x) (mem_atTop z))
    fun _ ⟨hxy, hzy⟩ => lt_of_le_not_le hxy fun hyx => hz (hzy.trans hyx)

Membership of Open Upper Set in `atTop` Filter for No-Top Orders

Informal description

For any preorder $\alpha$ with no top element and any element $x \in \alpha$, the left-open right-infinite interval $(x, \infty)$ belongs to the `atTop` filter on $\alpha$.

Filter.mem_atBot theorem

[Preorder α] (a : α) : {b : α | b ≤ a} ∈ @atBot α _

Full source

theorem mem_atBot [Preorder α] (a : α) : { b : α | b ≤ a }{ b : α | b ≤ a } ∈ @atBot α _ :=
  mem_iInf_of_mem a <| Subset.refl _

Membership of Lower Set in `atBot` Filter

Informal description

For any element $a$ in a preorder $\alpha$, the set $\{b \in \alpha \mid b \leq a\}$ belongs to the filter `atBot` on $\alpha$.

Filter.Iic_mem_atBot theorem

[Preorder α] (a : α) : Iic a ∈ (atBot : Filter α)

Full source

theorem Iic_mem_atBot [Preorder α] (a : α) : IicIic a ∈ (atBot : Filter α) :=
  mem_atBot a

Membership of Left-Infinite Interval in `atBot` Filter

Informal description

For any element $a$ in a preorder $\alpha$, the left-infinite right-closed interval $(-\infty, a]$ belongs to the filter `atBot` on $\alpha$.

Filter.Iio_mem_atBot theorem

[Preorder α] [NoBotOrder α] (x : α) : Iio x ∈ (atBot : Filter α)

Full source

theorem Iio_mem_atBot [Preorder α] [NoBotOrder α] (x : α) : IioIio x ∈ (atBot : Filter α) :=
  let ⟨z, hz⟩ := exists_not_ge x
  mem_of_superset (inter_mem (mem_atBot x) (mem_atBot z))
    fun _ ⟨hyx, hyz⟩ => lt_of_le_not_le hyx fun hxy => hz (hxy.trans hyz)

Membership of Left-Open Interval in `atBot` Filter for Orders without Bottom Elements

Informal description

For any element $x$ in a preorder $\alpha$ with no bottom element, the left-infinite right-open interval $(-\infty, x) = \{y \in \alpha \mid y < x\}$ belongs to the `atBot` filter on $\alpha$.

Filter.eventually_ge_atTop theorem

[Preorder α] (a : α) : ∀ᶠ x in atTop, a ≤ x

Full source

theorem eventually_ge_atTop [Preorder α] (a : α) : ∀ᶠ x in atTop, a ≤ x :=
  mem_atTop a

Eventual Lower Bound in `atTop` Filter

Informal description

For any element $a$ in a preorder $\alpha$, the filter `atTop` on $\alpha$ eventually contains all elements $x$ such that $a \leq x$.

Filter.eventually_le_atBot theorem

[Preorder α] (a : α) : ∀ᶠ x in atBot, x ≤ a

Full source

theorem eventually_le_atBot [Preorder α] (a : α) : ∀ᶠ x in atBot, x ≤ a :=
  mem_atBot a

Eventual Lower Bound in `atBot` Filter

Informal description

For any element $a$ in a preorder $\alpha$, the filter `atBot` on $\alpha$ eventually satisfies $x \leq a$ for all $x$ in the filter. In other words, $\forall_{\mathcal{F}_{\text{atBot}}} x, x \leq a$.

Filter.eventually_gt_atTop theorem

[Preorder α] [NoTopOrder α] (a : α) : ∀ᶠ x in atTop, a < x

Full source

theorem eventually_gt_atTop [Preorder α] [NoTopOrder α] (a : α) : ∀ᶠ x in atTop, a < x :=
  Ioi_mem_atTop a

Eventual Strict Upper Bound in `atTop` Filter for No-Top Orders

Informal description

For any preorder $\alpha$ with no top element and any element $a \in \alpha$, the filter `atTop` on $\alpha$ eventually contains all elements $x$ such that $a < x$.

Filter.eventually_ne_atTop theorem

[Preorder α] [NoTopOrder α] (a : α) : ∀ᶠ x in atTop, x ≠ a

Full source

theorem eventually_ne_atTop [Preorder α] [NoTopOrder α] (a : α) : ∀ᶠ x in atTop, x ≠ a :=
  (eventually_gt_atTop a).mono fun _ => ne_of_gt

Eventual Distinctness in `atTop` Filter for No-Top Orders

Informal description

For any preorder $\alpha$ with no top element and any element $a \in \alpha$, the filter `atTop` on $\alpha$ eventually contains all elements $x$ such that $x \neq a$.

Filter.eventually_lt_atBot theorem

[Preorder α] [NoBotOrder α] (a : α) : ∀ᶠ x in atBot, x < a

Full source

theorem eventually_lt_atBot [Preorder α] [NoBotOrder α] (a : α) : ∀ᶠ x in atBot, x < a :=
  Iio_mem_atBot a

Eventual Strict Inequality in `atBot` Filter for Orders without Bottom Elements

Informal description

For any element $a$ in a preorder $\alpha$ with no bottom element, the set of all elements $x \in \alpha$ such that $x < a$ is eventually in the `atBot` filter. In other words, $\forall a \in \alpha,\ \forall^\infty x \text{ in } \text{atBot},\ x < a$.

Filter.eventually_ne_atBot theorem

[Preorder α] [NoBotOrder α] (a : α) : ∀ᶠ x in atBot, x ≠ a

Full source

theorem eventually_ne_atBot [Preorder α] [NoBotOrder α] (a : α) : ∀ᶠ x in atBot, x ≠ a :=
  (eventually_lt_atBot a).mono fun _ => ne_of_lt

Eventual Non-Equality in `atBot` Filter for Orders without Bottom Elements

Informal description

For any element $a$ in a preorder $\alpha$ with no bottom element, the set of all elements $x \in \alpha$ such that $x \neq a$ is eventually in the `atBot` filter. In other words, $\forall a \in \alpha,\ \forall^\infty x \text{ in } \text{atBot},\ x \neq a$.

IsTop.atTop_eq theorem

[Preorder α] {a : α} (ha : IsTop a) : atTop = 𝓟 (Ici a)

Full source

theorem _root_.IsTop.atTop_eq [Preorder α] {a : α} (ha : IsTop a) : atTop = 𝓟 (Ici a) :=
  (iInf_le _ _).antisymm <| le_iInf fun b ↦ principal_mono.2 <| Ici_subset_Ici.2 <| ha b

Characterization of `atTop` Filter for Preorder with Top Element: $\text{atTop} = \mathcal{P}([a, \infty))$ when $a$ is top

Informal description

Let $\alpha$ be a preorder and $a \in \alpha$ be a top element (i.e., $b \leq a$ for all $b \in \alpha$). Then the filter `atTop` is equal to the principal filter generated by the interval $[a, \infty)$.

IsBot.atBot_eq theorem

[Preorder α] {a : α} (ha : IsBot a) : atBot = 𝓟 (Iic a)

Full source

theorem _root_.IsBot.atBot_eq [Preorder α] {a : α} (ha : IsBot a) : atBot = 𝓟 (Iic a) :=
  ha.toDual.atTop_eq

Characterization of `atBot` Filter for Preorder with Bottom Element: $\text{atBot} = \mathcal{P}((-\infty, a])$ when $a$ is bottom

Informal description

Let $\alpha$ be a preorder and $a \in \alpha$ be a bottom element (i.e., $a \leq b$ for all $b \in \alpha$). Then the filter `atBot` is equal to the principal filter generated by the left-infinite right-closed interval $(-\infty, a]$.

Filter.atTop_eq_generate_Ici theorem

[Preorder α] : atTop = generate (range (Ici (α := α)))

Full source

theorem atTop_eq_generate_Ici [Preorder α] : atTop = generate (range (Ici (α := α))) := by
  simp only [generate_eq_biInf, atTop, iInf_range]

Characterization of `atTop` as the Filter Generated by Intervals $[a, \infty)$

Informal description

For any preorder $\alpha$, the filter `atTop` is equal to the filter generated by the range of the function that maps each element $a \in \alpha$ to the left-closed right-infinite interval $[a, \infty)$. In other words, $$\text{atTop} = \text{generate} \left( \bigcup_{a \in \alpha} \{ [a, \infty) \} \right).$$

Filter.Frequently.forall_exists_of_atTop theorem

[Preorder α] {p : α → Prop} (h : ∃ᶠ x in atTop, p x) (a : α) : ∃ b ≥ a, p b

Full source

theorem Frequently.forall_exists_of_atTop [Preorder α] {p : α → Prop}
    (h : ∃ᶠ x in atTop, p x) (a : α) : ∃ b ≥ a, p b := by
  rw [Filter.Frequently] at h
  contrapose! h
  exact (eventually_ge_atTop a).mono h

Frequent Occurrence in `atTop` Filter Implies Existence Above Any Threshold

Informal description

Let $\alpha$ be a preorder and $p : \alpha \to \mathrm{Prop}$ be a predicate. If $p(x)$ holds frequently in the `atTop` filter (i.e., for infinitely many $x$ tending to infinity), then for any $a \in \alpha$, there exists $b \geq a$ such that $p(b)$ holds.

Filter.Frequently.forall_exists_of_atBot theorem

[Preorder α] {p : α → Prop} (h : ∃ᶠ x in atBot, p x) (a : α) : ∃ b ≤ a, p b

Full source

theorem Frequently.forall_exists_of_atBot [Preorder α] {p : α → Prop}
    (h : ∃ᶠ x in atBot, p x) (a : α) : ∃ b ≤ a, p b :=
  Frequently.forall_exists_of_atTop (α := αᵒᵈ) h _

Frequent Occurrence in `atBot` Filter Implies Existence Below Any Threshold

Informal description

Let $\alpha$ be a preorder and $p : \alpha \to \mathrm{Prop}$ be a predicate. If $p(x)$ holds frequently in the `atBot` filter (i.e., for infinitely many $x$ tending to negative infinity), then for any $a \in \alpha$, there exists $b \leq a$ such that $p(b)$ holds.

Filter.atTop_eq_generate_of_forall_exists_le theorem

[Preorder α] {s : Set α} (hs : ∀ x, ∃ y ∈ s, x ≤ y) : (atTop : Filter α) = generate (Ici '' s)

Full source

lemma atTop_eq_generate_of_forall_exists_le [Preorder α] {s : Set α} (hs : ∀ x, ∃ y ∈ s, x ≤ y) :
    (atTop : Filter α) = generate (IciIci '' s) := by
  rw [atTop_eq_generate_Ici]
  apply le_antisymm
  · rw [le_generate_iff]
    rintro - ⟨y, -, rfl⟩
    exact mem_generate_of_mem ⟨y, rfl⟩
  · rw [le_generate_iff]
    rintro - ⟨x, -, -, rfl⟩
    rcases hs x with ⟨y, ys, hy⟩
    have A : IciIci y ∈ generate (Ici '' s) := mem_generate_of_mem (mem_image_of_mem _ ys)
    have B : IciIci y ⊆ Ici x := Ici_subset_Ici.2 hy
    exact sets_of_superset (generate (IciIci '' s)) A B

Characterization of `atTop` Filter for Unbounded Above Sets

Informal description

Let $\alpha$ be a preorder and $s \subseteq \alpha$ be a subset such that for every $x \in \alpha$, there exists $y \in s$ with $x \leq y$. Then the filter `atTop` on $\alpha$ is equal to the filter generated by the image of $s$ under the function $Ici$, i.e., \[ \text{atTop} = \text{generate} \left( \{ [y, \infty) \mid y \in s \} \right). \]

Filter.atTop_eq_generate_of_not_bddAbove theorem

[LinearOrder α] {s : Set α} (hs : ¬BddAbove s) : (atTop : Filter α) = generate (Ici '' s)

Full source

lemma atTop_eq_generate_of_not_bddAbove [LinearOrder α] {s : Set α} (hs : ¬ BddAbove s) :
    (atTop : Filter α) = generate (IciIci '' s) := by
  refine atTop_eq_generate_of_forall_exists_le fun x ↦ ?_
  obtain ⟨y, hy, hy'⟩ := not_bddAbove_iff.mp hs x
  exact ⟨y, hy, hy'.le⟩

Characterization of `atTop` Filter for Unbounded Above Sets in Linear Orders

Informal description

Let $\alpha$ be a linearly ordered type and $s \subseteq \alpha$ be an unbounded above subset (i.e., for every $x \in \alpha$, there exists $y \in s$ with $x < y$). Then the filter `atTop` on $\alpha$ is equal to the filter generated by the collection of left-closed right-infinite intervals $[y, \infty)$ for $y \in s$: \[ \text{atTop} = \text{generate} \left( \{ [y, \infty) \mid y \in s \} \right). \]

Monotone.piecewise_eventually_eq_iUnion theorem

 {β : α → Type*} [Preorder ι] {s : ι → Set α} [∀ i, DecidablePred (· ∈ s i)] [DecidablePred (· ∈ ⋃ i, s i)]
  (hs : Monotone s) (f g : (a : α) → β a) (a : α) : ∀ᶠ i in atTop, (s i).piecewise f g a = (⋃ i, s i).piecewise f g a

Full source

theorem Monotone.piecewise_eventually_eq_iUnion {β : α → Type*} [Preorder ι] {s : ι → Set α}
    [∀ i, DecidablePred (· ∈ s i)] [DecidablePred (· ∈ ⋃ i, s i)]
    (hs : Monotone s) (f g : (a : α) → β a) (a : α) :
    ∀ᶠ i in atTop, (s i).piecewise f g a = (⋃ i, s i).piecewise f g a := by
  rcases em (∃ i, a ∈ s i) with ⟨i, hi⟩ | ha
  · refine (eventually_ge_atTop i).mono fun j hij ↦ ?_
    simp only [Set.piecewise_eq_of_mem, hs hij hi, subset_iUnion _ _ hi]
  · filter_upwards with i
    simp only [Set.piecewise_eq_of_not_mem, not_exists.1 ha i, mt mem_iUnion.1 ha,
      not_false_eq_true, exists_false]

Eventual Equality of Monotone Piecewise Functions with Union in `atTop` Filter

Informal description

Let $\alpha$ and $\iota$ be types with $\iota$ equipped with a preorder, and let $\beta : \alpha \to \text{Type}$ be a type family. Given a monotone family of sets $s : \iota \to \text{Set } \alpha$ (i.e., $i \leq j$ implies $s_i \subseteq s_j$) and functions $f, g : (a : \alpha) \to \beta a$, for any $a \in \alpha$, the piecewise function $(s_i).\text{piecewise}\ f\ g$ evaluated at $a$ eventually equals $(\bigcup_i s_i).\text{piecewise}\ f\ g$ evaluated at $a$ in the filter `atTop` on $\iota$. In other words, for any $a \in \alpha$, there exists $i_0 \in \iota$ such that for all $i \geq i_0$, \[ (s_i).\text{piecewise}\ f\ g\ a = (\bigcup_i s_i).\text{piecewise}\ f\ g\ a. \]

Antitone.piecewise_eventually_eq_iInter theorem

 {β : α → Type*} [Preorder ι] {s : ι → Set α} [∀ i, DecidablePred (· ∈ s i)] [DecidablePred (· ∈ ⋂ i, s i)]
  (hs : Antitone s) (f g : (a : α) → β a) (a : α) : ∀ᶠ i in atTop, (s i).piecewise f g a = (⋂ i, s i).piecewise f g a

Full source

theorem Antitone.piecewise_eventually_eq_iInter {β : α → Type*} [Preorder ι] {s : ι → Set α}
    [∀ i, DecidablePred (· ∈ s i)] [DecidablePred (· ∈ ⋂ i, s i)]
    (hs : Antitone s) (f g : (a : α) → β a) (a : α) :
    ∀ᶠ i in atTop, (s i).piecewise f g a = (⋂ i, s i).piecewise f g a := by
  classical
  convert ← (compl_anti.comp hs).piecewise_eventually_eq_iUnion g f a using 3
  · convert congr_fun (Set.piecewise_compl (s _) g f) a
  · simp only [(· ∘ ·), ← compl_iInter, Set.piecewise_compl]

Eventual Equality of Antitone Piecewise Functions with Intersection in `atTop` Filter

Informal description

Let $\alpha$ and $\iota$ be types with $\iota$ equipped with a preorder, and let $\beta : \alpha \to \text{Type}$ be a type family. Given an antitone family of sets $s : \iota \to \text{Set } \alpha$ (i.e., $i \leq j$ implies $s_j \subseteq s_i$) and functions $f, g : (a : \alpha) \to \beta a$, for any $a \in \alpha$, the piecewise function $(s_i).\text{piecewise}\ f\ g$ evaluated at $a$ eventually equals $(\bigcap_i s_i).\text{piecewise}\ f\ g$ evaluated at $a$ in the filter `atTop` on $\iota$. In other words, for any $a \in \alpha$, there exists $i_0 \in \iota$ such that for all $i \geq i_0$, \[ (s_i).\text{piecewise}\ f\ g\ a = (\bigcap_i s_i).\text{piecewise}\ f\ g\ a. \]