Mathlib.Topology.Order.LeftRight

frequently_lt_nhds theorem

(a : α) [NeBot (𝓝[<] a)] : ∃ᶠ x in 𝓝 a, x < a

Full source

lemma frequently_lt_nhds (a : α) [NeBot (𝓝[<] a)] : ∃ᶠ x in 𝓝 a, x < a :=
  frequently_iff_neBot.2 ‹_›

Frequent Elements Less Than a Point in Non-Trivial Left-Neighborhood

Informal description

For an element $a$ in a topological space $\alpha$ where the left-neighborhood filter $\mathcal{N}[<] a$ is non-trivial, there exist infinitely many elements $x$ in the neighborhood of $a$ such that $x < a$.

frequently_gt_nhds theorem

(a : α) [NeBot (𝓝[>] a)] : ∃ᶠ x in 𝓝 a, a < x

Full source

lemma frequently_gt_nhds (a : α) [NeBot (𝓝[>] a)] : ∃ᶠ x in 𝓝 a, a < x :=
  frequently_iff_neBot.2 ‹_›

Frequent Elements Greater Than a Point in Non-Trivial Right-Neighborhood

Informal description

For an element $a$ in a topological space $\alpha$ where the right-neighborhood filter $\mathcal{N}[>] a$ is non-trivial, there exist infinitely many elements $x$ in the neighborhood of $a$ such that $a < x$.

Filter.Eventually.exists_lt theorem

{a : α} [NeBot (𝓝[<] a)] {p : α → Prop} (h : ∀ᶠ x in 𝓝 a, p x) : ∃ b < a, p b

Full source

theorem Filter.Eventually.exists_lt {a : α} [NeBot (𝓝[<] a)] {p : α → Prop}
    (h : ∀ᶠ x in 𝓝 a, p x) : ∃ b < a, p b :=
  ((frequently_lt_nhds a).and_eventually h).exists

Existence of Element Less Than $a$ Satisfying Property in Non-Trivial Left-Neighborhood

Informal description

For any element $a$ in a topological space $\alpha$ where the left-neighborhood filter $\mathcal{N}[<] a$ is non-trivial, and for any property $p$ on $\alpha$, if $p(x)$ holds for all $x$ in some neighborhood of $a$, then there exists an element $b < a$ such that $p(b)$ holds.

Filter.Eventually.exists_gt theorem

{a : α} [NeBot (𝓝[>] a)] {p : α → Prop} (h : ∀ᶠ x in 𝓝 a, p x) : ∃ b > a, p b

Full source

theorem Filter.Eventually.exists_gt {a : α} [NeBot (𝓝[>] a)] {p : α → Prop}
    (h : ∀ᶠ x in 𝓝 a, p x) : ∃ b > a, p b :=
  ((frequently_gt_nhds a).and_eventually h).exists

Existence of Element Greater Than $a$ Satisfying Property in Non-Trivial Right-Neighborhood

Informal description

For any element $a$ in a topological space $\alpha$ where the right-neighborhood filter $\mathcal{N}[>] a$ is non-trivial, and for any property $p$ on $\alpha$, if $p(x)$ holds for all $x$ in some neighborhood of $a$, then there exists an element $b > a$ such that $p(b)$ holds.

nhdsWithin_Ici_neBot theorem

{a b : α} (H₂ : a ≤ b) : NeBot (𝓝[Ici a] b)

Full source

theorem nhdsWithin_Ici_neBot {a b : α} (H₂ : a ≤ b) : NeBot (𝓝[Ici a] b) :=
  nhdsWithin_neBot_of_mem H₂

Non-triviality of Neighborhood Filter in Right-Infinite Interval at Point $b$

Informal description

For any two elements $a$ and $b$ in a preorder $\alpha$ with $a \leq b$, the neighborhood filter within the left-closed right-infinite interval $[a, \infty)$ at the point $b$ is non-trivial (i.e., it does not contain the empty set).

nhdsGE_neBot instance

(a : α) : NeBot (𝓝[≥] a)

Full source

instance nhdsGE_neBot (a : α) : NeBot (𝓝[≥] a) := nhdsWithin_Ici_neBot (le_refl a)

Non-triviality of Neighborhood Filter at Point in Right-Infinite Interval

Informal description

For any element $a$ in a preorder $\alpha$, the neighborhood filter within the right-infinite interval $[a, \infty)$ at the point $a$ is non-trivial (i.e., it does not contain the empty set).

nhdsWithin_Ici_self_neBot theorem

(a : α) : NeBot (𝓝[≥] a)

Full source

@[deprecated nhdsGE_neBot (since := "2024-12-21")]
theorem nhdsWithin_Ici_self_neBot (a : α) : NeBot (𝓝[≥] a) := nhdsGE_neBot a

Non-triviality of Right Neighborhood Filter at a Point

Informal description

For any element $a$ in a preorder $\alpha$, the neighborhood filter of $a$ within the right-infinite interval $[a, \infty)$ is non-trivial (i.e., it does not contain the empty set).

nhdsWithin_Iic_neBot theorem

{a b : α} (H : a ≤ b) : NeBot (𝓝[Iic b] a)

Full source

theorem nhdsWithin_Iic_neBot {a b : α} (H : a ≤ b) : NeBot (𝓝[Iic b] a) :=
  nhdsWithin_neBot_of_mem H

Non-triviality of Neighborhood Filter within $(-\infty, b]$ at $a$ when $a \leq b$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ with $a \leq b$, the neighborhood filter of $a$ within the left-infinite right-closed interval $(-\infty, b]$ is non-trivial (i.e., it does not contain the empty set).

nhdsLE_neBot instance

(a : α) : NeBot (𝓝[≤] a)

Full source

instance nhdsLE_neBot (a : α) : NeBot (𝓝[≤] a) := nhdsWithin_Iic_neBot (le_refl a)

Non-triviality of the Left Neighborhood Filter at a Point

Informal description

For any element $a$ in a topological space $\alpha$ with a preorder, the neighborhood filter of $a$ restricted to the set of elements less than or equal to $a$ is non-trivial (i.e., it does not contain the empty set).

nhdsWithin_Iic_self_neBot theorem

(a : α) : NeBot (𝓝[≤] a)

Full source

@[deprecated nhdsLE_neBot (since := "2024-12-21")]
theorem nhdsWithin_Iic_self_neBot (a : α) : NeBot (𝓝[≤] a) := nhdsLE_neBot a

Non-triviality of the Left Neighborhood Filter at a Point in $(-\infty, a]$

Informal description

For any element $a$ in a topological space $\alpha$ with a preorder, the neighborhood filter of $a$ restricted to the left-infinite right-closed interval $(-\infty, a]$ is non-trivial (i.e., it does not contain the empty set).

nhdsLT_le_nhdsNE theorem

(a : α) : 𝓝[<] a ≤ 𝓝[≠] a

Full source

theorem nhdsLT_le_nhdsNE (a : α) : 𝓝[<] a ≤ 𝓝[≠] a :=
  nhdsWithin_mono a fun _ => ne_of_lt

Neighborhood Filter Comparison: Strictly Less Than vs. Not Equal To

Informal description

For any element $a$ in a topological space $\alpha$, the neighborhood filter of points strictly less than $a$ is finer than the neighborhood filter of points not equal to $a$, i.e., $\mathcal{N}_{<}(a) \leq \mathcal{N}_{\neq}(a)$.

nhdsGT_le_nhdsNE theorem

(a : α) : 𝓝[>] a ≤ 𝓝[≠] a

Full source

theorem nhdsGT_le_nhdsNE (a : α) : 𝓝[>] a ≤ 𝓝[≠] a := nhdsWithin_mono a fun _ => ne_of_gt

Right Neighborhood Filter is Finer than Punctured Neighborhood Filter

Informal description

For any element $a$ in a topological space $\alpha$, the neighborhood filter of $a$ restricted to the right-open interval $(a, \infty)$ is finer than the neighborhood filter of $a$ restricted to the complement of $\{a\}$. In other words, $\mathcal{N}_{>a} \leq \mathcal{N}_{\neq a}$.

IsAntichain.interior_eq_empty theorem

[∀ x : α, (𝓝[<] x).NeBot] {s : Set α} (hs : IsAntichain (· ≤ ·) s) : interior s = ∅

Full source

lemma IsAntichain.interior_eq_empty [∀ x : α, (𝓝[<] x).NeBot] {s : Set α}
    (hs : IsAntichain (· ≤ ·) s) : interior s = ∅ := by
  refine eq_empty_of_forall_not_mem fun x hx ↦ ?_
  have : ∀ᶠ y in 𝓝 x, y ∈ s := mem_interior_iff_mem_nhds.1 hx
  rcases this.exists_lt with ⟨y, hyx, hys⟩
  exact hs hys (interior_subset hx) hyx.ne hyx.le

Empty Interior of Antichains in Spaces with Non-Trivial Left-Neighborhoods

Informal description

Let $\alpha$ be a topological space where for every $x \in \alpha$, the left-neighborhood filter $\mathcal{N}[<] x$ is non-trivial. For any antichain $s \subseteq \alpha$ with respect to the partial order $\leq$, the interior of $s$ is empty, i.e., $\text{interior}(s) = \emptyset$.

IsAntichain.interior_eq_empty' theorem

[∀ x : α, (𝓝[>] x).NeBot] {s : Set α} (hs : IsAntichain (· ≤ ·) s) : interior s = ∅

Full source

lemma IsAntichain.interior_eq_empty' [∀ x : α, (𝓝[>] x).NeBot] {s : Set α}
    (hs : IsAntichain (· ≤ ·) s) : interior s = ∅ :=
  have : ∀ x : αᵒᵈ, NeBot (𝓝[<] x) := ‹_›
  hs.to_dual.interior_eq_empty

Empty Interior of Antichains in Spaces with Non-Trivial Right-Neighborhoods

Informal description

Let $\alpha$ be a topological space where for every $x \in \alpha$, the right-neighborhood filter $\mathcal{N}[>] x$ is non-trivial. For any antichain $s \subseteq \alpha$ with respect to the partial order $\leq$, the interior of $s$ is empty, i.e., $\text{interior}(s) = \emptyset$.

continuousWithinAt_Ioi_iff_Ici theorem

{a : α} {f : α → β} : ContinuousWithinAt f (Ioi a) a ↔ ContinuousWithinAt f (Ici a) a

Full source

theorem continuousWithinAt_Ioi_iff_Ici {a : α} {f : α → β} :
    ContinuousWithinAtContinuousWithinAt f (Ioi a) a ↔ ContinuousWithinAt f (Ici a) a := by
  simp only [← Ici_diff_left, continuousWithinAt_diff_self]

Equivalence of Right Continuity Definitions: $(a, \infty)$ vs $[a, \infty)$

Informal description

For a function $f : \alpha \to \beta$ and a point $a \in \alpha$, the following are equivalent: 1. $f$ is continuous at $a$ when restricted to the open right interval $(a, \infty)$. 2. $f$ is continuous at $a$ when restricted to the closed right interval $[a, \infty)$.

continuousWithinAt_Iio_iff_Iic theorem

{a : α} {f : α → β} : ContinuousWithinAt f (Iio a) a ↔ ContinuousWithinAt f (Iic a) a

Full source

theorem continuousWithinAt_Iio_iff_Iic {a : α} {f : α → β} :
    ContinuousWithinAtContinuousWithinAt f (Iio a) a ↔ ContinuousWithinAt f (Iic a) a :=
  @continuousWithinAt_Ioi_iff_Ici αᵒᵈ _ _ _ _ _ f

Equivalence of Left Continuity Definitions: $(-\infty, a)$ vs $(-\infty, a]$

Informal description

For a function $f : \alpha \to \beta$ and a point $a \in \alpha$, the following are equivalent: 1. $f$ is continuous at $a$ when restricted to the open left interval $(-\infty, a)$. 2. $f$ is continuous at $a$ when restricted to the closed left interval $(-\infty, a]$.

nhdsLE_sup_nhdsGE theorem

(a : α) : 𝓝[≤] a ⊔ 𝓝[≥] a = 𝓝 a

Full source

theorem nhdsLE_sup_nhdsGE (a : α) : 𝓝[≤] a𝓝[≤] a ⊔ 𝓝[≥] a = 𝓝 a := by
  rw [← nhdsWithin_union, Iic_union_Ici, nhdsWithin_univ]

Neighborhood Filter Decomposition: $\mathcal{N}_{\leq}(a) \sqcup \mathcal{N}_{\geq}(a) = \mathcal{N}(a)$

Informal description

For any element $a$ in a topological space $\alpha$, the supremum of the left neighborhood filter $\mathcal{N}_{\leq}(a)$ (consisting of neighborhoods of $a$ restricted to $(-\infty, a]$) and the right neighborhood filter $\mathcal{N}_{\geq}(a)$ (consisting of neighborhoods of $a$ restricted to $[a, \infty)$) equals the full neighborhood filter $\mathcal{N}(a)$ of $a$.

nhdsLT_sup_nhdsGE theorem

(a : α) : 𝓝[<] a ⊔ 𝓝[≥] a = 𝓝 a

Full source

theorem nhdsLT_sup_nhdsGE (a : α) : 𝓝[<] a𝓝[<] a ⊔ 𝓝[≥] a = 𝓝 a := by
  rw [← nhdsWithin_union, Iio_union_Ici, nhdsWithin_univ]

Neighborhood Decomposition: $\mathcal{N}_{<}(a) \sqcup \mathcal{N}_{\geq}(a) = \mathcal{N}(a)$

Informal description

For any element $a$ in a topological space $\alpha$, the supremum of the left neighborhood filter $\mathcal{N}_{<}(a)$ (consisting of neighborhoods of $a$ restricted to $(-\infty, a)$) and the right neighborhood filter $\mathcal{N}_{\geq}(a)$ (consisting of neighborhoods of $a$ restricted to $[a, \infty)$) equals the full neighborhood filter $\mathcal{N}(a)$ of $a$.

nhdsLE_sup_nhdsGT theorem

(a : α) : 𝓝[≤] a ⊔ 𝓝[>] a = 𝓝 a

Full source

theorem nhdsLE_sup_nhdsGT (a : α) : 𝓝[≤] a𝓝[≤] a ⊔ 𝓝[>] a = 𝓝 a := by
  rw [← nhdsWithin_union, Iic_union_Ioi, nhdsWithin_univ]

Neighborhood Decomposition: $\mathcal{N}_{\leq}(a) \sqcup \mathcal{N}_{>}(a) = \mathcal{N}(a)$

Informal description

For any element $a$ in a topological space $\alpha$, the supremum of the left neighborhood filter $\mathcal{N}_{\leq}(a)$ (consisting of neighborhoods of $a$ restricted to $(-\infty, a]$) and the right neighborhood filter $\mathcal{N}_{>}(a)$ (consisting of neighborhoods of $a$ restricted to $(a, \infty)$) equals the full neighborhood filter $\mathcal{N}(a)$ of $a$.

nhdsLT_sup_nhdsGT theorem

(a : α) : 𝓝[<] a ⊔ 𝓝[>] a = 𝓝[≠] a

Full source

theorem nhdsLT_sup_nhdsGT (a : α) : 𝓝[<] a𝓝[<] a ⊔ 𝓝[>] a = 𝓝[≠] a := by
  rw [← nhdsWithin_union, Iio_union_Ioi]

Punctured Neighborhood as Supremum of Left and Right Neighborhoods

Informal description

For any element $a$ in a topological space $\alpha$, the supremum of the left neighborhood filter $\mathcal{N}_{<}(a)$ (consisting of neighborhoods of $a$ restricted to $(-\infty, a)$) and the right neighborhood filter $\mathcal{N}_{>}(a)$ (consisting of neighborhoods of $a$ restricted to $(a, \infty)$) equals the punctured neighborhood filter $\mathcal{N}_{\neq}(a)$ (consisting of neighborhoods of $a$ excluding $a$ itself).

nhdsWithin_right_sup_nhds_singleton theorem

(a : α) : 𝓝[>] a ⊔ 𝓝[{ a }] a = 𝓝[≥] a

Full source

lemma nhdsWithin_right_sup_nhds_singleton (a : α) :
    𝓝[>] a𝓝[>] a ⊔ 𝓝[{a}] a = 𝓝[≥] a := by
  simp only [union_singleton, Ioi_insert, ← nhdsWithin_union]

Neighborhood Decomposition: $\mathcal{N}_{>}(a) \sqcup \mathcal{N}_{\{a\}}(a) = \mathcal{N}_{\geq}(a)$

Informal description

For any element $a$ in a topological space $\alpha$, the supremum of the right neighborhood filter $\mathcal{N}_{>}(a)$ (consisting of neighborhoods of $a$ restricted to $(a, \infty)$) and the singleton neighborhood filter $\mathcal{N}_{\{a\}}(a)$ equals the right-closed neighborhood filter $\mathcal{N}_{\geq}(a)$ (consisting of neighborhoods of $a$ restricted to $[a, \infty)$).

continuousAt_iff_continuous_left_right theorem

{a : α} {f : α → β} : ContinuousAt f a ↔ ContinuousWithinAt f (Iic a) a ∧ ContinuousWithinAt f (Ici a) a

Full source

theorem continuousAt_iff_continuous_left_right {a : α} {f : α → β} :
    ContinuousAtContinuousAt f a ↔ ContinuousWithinAt f (Iic a) a ∧ ContinuousWithinAt f (Ici a) a := by
  simp only [ContinuousWithinAt, ContinuousAt, ← tendsto_sup, nhdsLE_sup_nhdsGE]

Characterization of Continuity via Left and Right Continuity: $f$ continuous at $a$ $\iff$ $f$ left and right continuous at $a$

Informal description

A function $f : \alpha \to \beta$ is continuous at a point $a \in \alpha$ if and only if it is both left continuous and right continuous at $a$, where left continuity means continuity within the left-infinite right-closed interval $(-\infty, a]$ and right continuity means continuity within the left-closed right-infinite interval $[a, \infty)$.

continuousAt_iff_continuous_left'_right' theorem

{a : α} {f : α → β} : ContinuousAt f a ↔ ContinuousWithinAt f (Iio a) a ∧ ContinuousWithinAt f (Ioi a) a

Full source

theorem continuousAt_iff_continuous_left'_right' {a : α} {f : α → β} :
    ContinuousAtContinuousAt f a ↔ ContinuousWithinAt f (Iio a) a ∧ ContinuousWithinAt f (Ioi a) a := by
  rw [continuousWithinAt_Ioi_iff_Ici, continuousWithinAt_Iio_iff_Iic,
    continuousAt_iff_continuous_left_right]

Characterization of Continuity via Open Left and Right Continuity: $f$ continuous at $a$ $\iff$ $f$ left and right continuous in open intervals

Informal description

A function $f : \alpha \to \beta$ is continuous at a point $a \in \alpha$ if and only if it is both left continuous at $a$ when restricted to the open left interval $(-\infty, a)$ and right continuous at $a$ when restricted to the open right interval $(a, \infty)$.

Tags