Mathlib.Order.Filter.AtTopBot.Disjoint

Filter.disjoint_atBot_principal_Ioi theorem

[Preorder α] (x : α) : Disjoint atBot (𝓟 (Ioi x))

Full source

theorem disjoint_atBot_principal_Ioi [Preorder α] (x : α) : Disjoint atBot (𝓟 (Ioi x)) :=
  disjoint_of_disjoint_of_mem (Iic_disjoint_Ioi le_rfl) (Iic_mem_atBot x) (mem_principal_self _)

Disjointness of `atBot` and the principal filter of $(x, \infty)$

Informal description

For any element $x$ in a preorder $\alpha$, the filter `atBot` (representing the limit at negative infinity) is disjoint from the principal filter generated by the left-open right-infinite interval $(x, \infty)$. In other words, there is no element that is both eventually less than or equal to all elements and strictly greater than $x$.

Filter.disjoint_atTop_principal_Iio theorem

[Preorder α] (x : α) : Disjoint atTop (𝓟 (Iio x))

Full source

theorem disjoint_atTop_principal_Iio [Preorder α] (x : α) : Disjoint atTop (𝓟 (Iio x)) :=
  @disjoint_atBot_principal_Ioi αᵒᵈ _ _

Disjointness of `atTop` and the principal filter of $(-\infty, x)$

Informal description

For any element $x$ in a preorder $\alpha$, the filter `atTop` (representing the limit tending to positive infinity) is disjoint from the principal filter generated by the left-infinite right-open interval $(-\infty, x)$. In other words, there is no element that is both eventually greater than or equal to all elements and strictly less than $x$.

Filter.disjoint_atTop_principal_Iic theorem

[Preorder α] [NoTopOrder α] (x : α) : Disjoint atTop (𝓟 (Iic x))

Full source

theorem disjoint_atTop_principal_Iic [Preorder α] [NoTopOrder α] (x : α) :
    Disjoint atTop (𝓟 (Iic x)) :=
  disjoint_of_disjoint_of_mem (Iic_disjoint_Ioi le_rfl).symm (Ioi_mem_atTop x)
    (mem_principal_self _)

Disjointness of `atTop` Filter and Principal Filter of $(-\infty, x]$ in No-Top Orders

Informal description

For any preorder $\alpha$ with no top element and any element $x \in \alpha$, the filter `atTop` (representing the limit tending to positive infinity) is disjoint from the principal filter generated by the left-infinite right-closed interval $(-\infty, x]$.

Filter.disjoint_atBot_principal_Ici theorem

[Preorder α] [NoBotOrder α] (x : α) : Disjoint atBot (𝓟 (Ici x))

Full source

theorem disjoint_atBot_principal_Ici [Preorder α] [NoBotOrder α] (x : α) :
    Disjoint atBot (𝓟 (Ici x)) :=
  @disjoint_atTop_principal_Iic αᵒᵈ _ _ _

Disjointness of `atBot` and Principal Filter of $[x, \infty)$ in No-Bottom Orders

Informal description

For any preorder $\alpha$ with no bottom element and any element $x \in \alpha$, the filter `atBot` (representing the limit tending to negative infinity) is disjoint from the principal filter generated by the right-infinite left-closed interval $[x, \infty)$.

Filter.disjoint_pure_atTop theorem

[Preorder α] [NoTopOrder α] (x : α) : Disjoint (pure x) atTop

Full source

theorem disjoint_pure_atTop [Preorder α] [NoTopOrder α] (x : α) : Disjoint (pure x) atTop :=
  Disjoint.symm <| (disjoint_atTop_principal_Iic x).mono_right <| le_principal_iff.2 <|
    mem_pure.2 right_mem_Iic

Disjointness of Singleton Principal Filter and `atTop` Filter in No-Top Orders

Informal description

For any preorder $\alpha$ with no top element and any element $x \in \alpha$, the principal filter generated by the singleton set $\{x\}$ is disjoint from the `atTop` filter (representing the limit tending to positive infinity).

Filter.disjoint_pure_atBot theorem

[Preorder α] [NoBotOrder α] (x : α) : Disjoint (pure x) atBot

Full source

theorem disjoint_pure_atBot [Preorder α] [NoBotOrder α] (x : α) : Disjoint (pure x) atBot :=
  @disjoint_pure_atTop αᵒᵈ _ _ _

Disjointness of Singleton Principal Filter and `atBot` Filter in No-Bottom Orders

Informal description

For any preorder $\alpha$ with no bottom element and any element $x \in \alpha$, the principal filter generated by the singleton set $\{x\}$ is disjoint from the `atBot` filter (representing the limit tending to negative infinity).

Filter.disjoint_atBot_atTop theorem

[PartialOrder α] [Nontrivial α] : Disjoint (atBot : Filter α) atTop

Full source

theorem disjoint_atBot_atTop [PartialOrder α] [Nontrivial α] :
    Disjoint (atBot : Filter α) atTop := by
  rcases exists_pair_ne α with ⟨x, y, hne⟩
  by_cases hle : x ≤ y
  · refine disjoint_of_disjoint_of_mem ?_ (Iic_mem_atBot x) (Ici_mem_atTop y)
    exact Iic_disjoint_Ici.2 (hle.lt_of_ne hne).not_le
  · refine disjoint_of_disjoint_of_mem ?_ (Iic_mem_atBot y) (Ici_mem_atTop x)
    exact Iic_disjoint_Ici.2 hle

Disjointness of `atBot` and `atTop` Filters in Nontrivial Partial Orders

Informal description

For any nontrivial partially ordered set $\alpha$, the filters `atBot` and `atTop` are disjoint. That is, there is no element $x \in \alpha$ that is both in the `atBot` filter (tending to negative infinity) and the `atTop` filter (tending to positive infinity).

Filter.disjoint_atTop_atBot theorem

[PartialOrder α] [Nontrivial α] : Disjoint (atTop : Filter α) atBot

Full source

theorem disjoint_atTop_atBot [PartialOrder α] [Nontrivial α] : Disjoint (atTop : Filter α) atBot :=
  disjoint_atBot_atTop.symm

Disjointness of $\text{atTop}$ and $\text{atBot}$ Filters in Nontrivial Partial Orders

Informal description

For any nontrivial partially ordered set $\alpha$, the filters $\text{atTop}$ (tending to positive infinity) and $\text{atBot}$ (tending to negative infinity) are disjoint. That is, there is no element $x \in \alpha$ that is both in the $\text{atTop}$ filter and the $\text{atBot}$ filter.