Mathlib.Topology.Order.OrderClosed

ClosedIicTopology structure

(α : Type*) [TopologicalSpace α] [Preorder α]

Full source

/-- If `α` is a topological space and a preorder, `ClosedIicTopology α` means that `Iic a` is
closed for all `a : α`. -/
class ClosedIicTopology (α : Type*) [TopologicalSpace α] [Preorder α] : Prop where
  /-- For any `a`, the set `(-∞, a]` is closed. -/
  isClosed_Iic (a : α) : IsClosed (Iic a)

Closed lower interval topology

Informal description

A topological space $\alpha$ equipped with a preorder is said to satisfy the `ClosedIicTopology` property if for every element $a \in \alpha$, the set $\{x \in \alpha \mid x \leq a\}$ (denoted as $\text{Iic } a$) is closed in the topology of $\alpha$.

ClosedIciTopology structure

(α : Type*) [TopologicalSpace α] [Preorder α]

Full source

/-- If `α` is a topological space and a preorder, `ClosedIciTopology α` means that `Ici a` is
closed for all `a : α`. -/
class ClosedIciTopology (α : Type*) [TopologicalSpace α] [Preorder α] : Prop where
  /-- For any `a`, the set `[a, +∞)` is closed. -/
  isClosed_Ici (a : α) : IsClosed (Ici a)

Closed upper interval topology

Informal description

A topological space $\alpha$ equipped with a preorder is said to satisfy the `ClosedIciTopology` property if for every element $a \in \alpha$, the closed interval $[a, +\infty)$ (denoted as `Set.Ici a`) is a closed set in the topology.

OrderClosedTopology structure

(α : Type*) [TopologicalSpace α] [Preorder α]

Full source

/-- A topology on a set which is both a topological space and a preorder is _order-closed_ if the
set of points `(x, y)` with `x ≤ y` is closed in the product space. We introduce this as a mixin.
This property is satisfied for the order topology on a linear order, but it can be satisfied more
generally, and suffices to derive many interesting properties relating order and topology. -/
class OrderClosedTopology (α : Type*) [TopologicalSpace α] [Preorder α] : Prop where
  /-- The set `{ (x, y) | x ≤ y }` is a closed set. -/
  isClosed_le' : IsClosed { p : α × α | p.1 ≤ p.2 }

Order-Closed Topology

Informal description

A topology on a set which is both a topological space and a preorder is called *order-closed* if the set of points $(x, y)$ with $x \leq y$ is closed in the product space. This property is satisfied for the order topology on a linear order, but it can be satisfied more generally, and suffices to derive many interesting properties relating order and topology.

instFirstCountableTopologyOrderDual instance

[TopologicalSpace α] [h : FirstCountableTopology α] : FirstCountableTopology αᵒᵈ

Full source

instance [TopologicalSpace α] [h : FirstCountableTopology α] : FirstCountableTopology αᵒᵈ := h

First-Countability of Order Dual Topological Spaces

Informal description

For any topological space $\alpha$ with a preorder and first-countable topology, the order dual $\alpha^{\text{op}}$ also has a first-countable topology.

instSecondCountableTopologyOrderDual instance

[TopologicalSpace α] [h : SecondCountableTopology α] : SecondCountableTopology αᵒᵈ

Full source

instance [TopologicalSpace α] [h : SecondCountableTopology α] : SecondCountableTopology αᵒᵈ := h

Second-Countability of Order Dual Topological Space

Informal description

For any topological space $\alpha$ with a preorder and second-countable topology, the order dual $\alpha^{\text{op}}$ also has a second-countable topology.

Dense.orderDual theorem

[TopologicalSpace α] {s : Set α} (hs : Dense s) : Dense (OrderDual.ofDual ⁻¹' s)

Full source

theorem Dense.orderDual [TopologicalSpace α] {s : Set α} (hs : Dense s) :
    Dense (OrderDual.ofDualOrderDual.ofDual ⁻¹' s) :=
  hs

Density Preservation under Order Duality

Informal description

For any topological space $\alpha$ with a preorder, if a subset $s$ is dense in $\alpha$, then its preimage under the order dual operation (i.e., the same subset considered in the order dual space $\alpha^{\text{op}}$) is also dense.

BddAbove.of_closure theorem

: BddAbove (closure s) → BddAbove s

Full source

protected lemma BddAbove.of_closure : BddAbove (closure s) → BddAbove s :=
  BddAbove.mono subset_closure

Boundedness Above is Preserved by Closure

Informal description

If the closure of a set $s$ in a topological space is bounded above, then $s$ itself is bounded above.

BddBelow.of_closure theorem

: BddBelow (closure s) → BddBelow s

Full source

protected lemma BddBelow.of_closure : BddBelow (closure s) → BddBelow s :=
  BddBelow.mono subset_closure

Bounded Below Property Preserved by Closure

Informal description

If the closure of a set $s$ in a topological space is bounded below, then $s$ itself is bounded below.

isClosed_Iic theorem

: IsClosed (Iic a)

Full source

theorem isClosed_Iic : IsClosed (Iic a) :=
  ClosedIicTopology.isClosed_Iic a

Closedness of Left-Infinite Right-Closed Interval in `ClosedIicTopology`

Informal description

For any element $a$ in a topological space $\alpha$ with a preorder and the `ClosedIicTopology` property, the left-infinite right-closed interval $(-\infty, a]$ (denoted as $\text{Iic } a$) is a closed set in the topology of $\alpha$.

instClosedIciTopologyOrderDual instance

: ClosedIciTopology αᵒᵈ

Full source

instance : ClosedIciTopology αᵒᵈ where
  isClosed_Ici _ := isClosed_Iic (α := α)

Order Dual Preserves Closed Upper Interval Topology

Informal description

The order dual $\alpha^\mathrm{op}$ of a topological space $\alpha$ with a preorder has the `ClosedIciTopology` property, meaning that for every element $a \in \alpha^\mathrm{op}$, the closed interval $[a, +\infty)$ in $\alpha^\mathrm{op}$ is a closed set in the topology.

closure_Iic theorem

(a : α) : closure (Iic a) = Iic a

Full source

@[simp]
theorem closure_Iic (a : α) : closure (Iic a) = Iic a :=
  isClosed_Iic.closure_eq

Closure of Left-Infinite Right-Closed Interval in `ClosedIicTopology`

Informal description

For any element $a$ in a topological space $\alpha$ with a preorder and the `ClosedIicTopology` property, the closure of the left-infinite right-closed interval $(-\infty, a]$ is equal to itself, i.e., $\overline{(-\infty, a]} = (-\infty, a]$.

le_of_tendsto_of_frequently theorem

{x : Filter β} (lim : Tendsto f x (𝓝 a)) (h : ∃ᶠ c in x, f c ≤ b) : a ≤ b

Full source

theorem le_of_tendsto_of_frequently {x : Filter β} (lim : Tendsto f x (𝓝 a))
    (h : ∃ᶠ c in x, f c ≤ b) : a ≤ b :=
  isClosed_Iic.mem_of_frequently_of_tendsto h lim

Limit Inequality from Frequent Bounds in `ClosedIicTopology`

Informal description

Let $f : \beta \to \alpha$ be a function from a topological space $\beta$ to a preordered topological space $\alpha$ with the `ClosedIicTopology` property. If $f$ tends to $a$ along a filter $x$ on $\beta$, and there exists a frequently occurring $c \in \beta$ such that $f(c) \leq b$, then $a \leq b$.

le_of_tendsto theorem

{x : Filter β} [NeBot x] (lim : Tendsto f x (𝓝 a)) (h : ∀ᶠ c in x, f c ≤ b) : a ≤ b

Full source

theorem le_of_tendsto {x : Filter β} [NeBot x] (lim : Tendsto f x (𝓝 a))
    (h : ∀ᶠ c in x, f c ≤ b) : a ≤ b :=
  isClosed_Iic.mem_of_tendsto lim h

Limit Inequality from Eventual Bounds in Closed Lower Interval Topology

Informal description

Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property, and let $\beta$ be another topological space. Given a function $f : \beta \to \alpha$, a filter $x$ on $\beta$ that is not the trivial filter, and elements $a, b \in \alpha$, if $f$ tends to $a$ along $x$ and eventually $f(c) \leq b$ for all $c$ in $x$, then $a \leq b$.

le_of_tendsto' theorem

{x : Filter β} [NeBot x] (lim : Tendsto f x (𝓝 a)) (h : ∀ c, f c ≤ b) : a ≤ b

Full source

theorem le_of_tendsto' {x : Filter β} [NeBot x] (lim : Tendsto f x (𝓝 a))
    (h : ∀ c, f c ≤ b) : a ≤ b :=
  le_of_tendsto lim (Eventually.of_forall h)

Limit Inequality from Uniform Bounds in Closed Lower Interval Topology

Informal description

Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property, and let $\beta$ be another topological space. Given a function $f : \beta \to \alpha$, a filter $x$ on $\beta$ that is not the trivial filter, and elements $a, b \in \alpha$, if $f$ tends to $a$ along $x$ and $f(c) \leq b$ for all $c \in \beta$, then $a \leq b$.

upperBounds_closure theorem

(s : Set α) : upperBounds (closure s : Set α) = upperBounds s

Full source

@[simp] lemma upperBounds_closure (s : Set α) : upperBounds (closure s : Set α) = upperBounds s :=
  ext fun a ↦ by simp_rw [mem_upperBounds_iff_subset_Iic, isClosed_Iic.closure_subset_iff]

Upper Bounds of Closure Equal Upper Bounds of Set in Closed Lower Interval Topology

Informal description

For any subset $s$ of a topological space $\alpha$ with a preorder and the `ClosedIicTopology` property, the set of upper bounds of the closure of $s$ is equal to the set of upper bounds of $s$ itself. In other words, $\text{upperBounds}(\overline{s}) = \text{upperBounds}(s)$.

bddAbove_closure theorem

: BddAbove (closure s) ↔ BddAbove s

Full source

@[simp] lemma bddAbove_closure : BddAboveBddAbove (closure s) ↔ BddAbove s := by
  simp_rw [BddAbove, upperBounds_closure]

Boundedness Above is Preserved by Closure in Closed Lower Interval Topology

Informal description

For any subset $s$ of a topological space $\alpha$ with a preorder and the `ClosedIicTopology` property, the closure of $s$ is bounded above if and only if $s$ is bounded above. In other words, $\overline{s}$ is bounded above $\iff$ $s$ is bounded above.

disjoint_nhds_atBot_iff theorem

: Disjoint (𝓝 a) atBot ↔ ¬IsBot a

Full source

@[simp]
theorem disjoint_nhds_atBot_iff : DisjointDisjoint (𝓝 a) atBot ↔ ¬IsBot a := by
  constructor
  · intro hd hbot
    rw [hbot.atBot_eq, disjoint_principal_right] at hd
    exact mem_of_mem_nhds hd le_rfl
  · simp only [IsBot, not_forall]
    rintro ⟨b, hb⟩
    refine disjoint_of_disjoint_of_mem disjoint_compl_left ?_ (Iic_mem_atBot b)
    exact isClosed_Iic.isOpen_compl.mem_nhds hb

Disjointness of Neighborhood and Bottom Filters Characterizes Non-Bottom Elements

Informal description

For any element $a$ in a topological space $\alpha$ with a preorder and the `ClosedIicTopology` property, the neighborhood filter $\mathcal{N}(a)$ and the filter `atBot` (the filter of sets containing all elements less than or equal to some element) are disjoint if and only if $a$ is not the least element in $\alpha$.

IsLUB.range_of_tendsto theorem

{F : Filter β} [F.NeBot] (hle : ∀ i, f i ≤ a) (hlim : Tendsto f F (𝓝 a)) : IsLUB (range f) a

Full source

theorem IsLUB.range_of_tendsto {F : Filter β} [F.NeBot] (hle : ∀ i, f i ≤ a)
    (hlim : Tendsto f F (𝓝 a)) : IsLUB (range f) a :=
  ⟨forall_mem_range.mpr hle, fun _c hc ↦ le_of_tendsto' hlim fun i ↦ hc <| mem_range_self i⟩

Least Upper Bound of Range via Limit in Closed Lower Interval Topology

Informal description

Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property, and let $\beta$ be another topological space. Given a function $f : \beta \to \alpha$, a non-trivial filter $F$ on $\beta$, and an element $a \in \alpha$, if $f(i) \leq a$ for all $i \in \beta$ and $f$ tends to $a$ along $F$, then $a$ is the least upper bound of the range of $f$.

disjoint_nhds_atBot theorem

(a : α) : Disjoint (𝓝 a) atBot

Full source

theorem disjoint_nhds_atBot (a : α) : Disjoint (𝓝 a) atBot := by simp

Disjointness of Neighborhood and Bottom Filters in Closed Lower Interval Topology

Informal description

For any element $a$ in a topological space $\alpha$ with a preorder and the `ClosedIicTopology` property, the neighborhood filter $\mathcal{N}(a)$ and the filter `atBot` (the filter of sets containing all elements less than or equal to some element) are disjoint.

inf_nhds_atBot theorem

(a : α) : 𝓝 a ⊓ atBot = ⊥

Full source

@[simp]
theorem inf_nhds_atBot (a : α) : 𝓝𝓝 a ⊓ atBot = ⊥ := (disjoint_nhds_atBot a).eq_bot

Infimum of Neighborhood and Bottom Filters is Bottom in Closed Lower Interval Topology

Informal description

For any element $a$ in a topological space $\alpha$ with a preorder and the `ClosedIicTopology` property, the infimum of the neighborhood filter $\mathcal{N}(a)$ and the filter `atBot` is the bottom filter $\bot$. In other words, $\mathcal{N}(a) \sqcap \text{atBot} = \bot$.

not_tendsto_nhds_of_tendsto_atBot theorem

(hf : Tendsto f l atBot) (a : α) : ¬Tendsto f l (𝓝 a)

Full source

theorem not_tendsto_nhds_of_tendsto_atBot (hf : Tendsto f l atBot) (a : α) : ¬Tendsto f l (𝓝 a) :=
  hf.not_tendsto (disjoint_nhds_atBot a).symm

Non-convergence to Neighborhood Filters under Bottom Filter Convergence

Informal description

Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property. If a function $f$ tends to the filter `atBot` (the filter of sets containing all elements less than or equal to some element), then $f$ does not tend to any neighborhood filter $\mathcal{N}(a)$ for any $a \in \alpha$.

not_tendsto_atBot_of_tendsto_nhds theorem

(hf : Tendsto f l (𝓝 a)) : ¬Tendsto f l atBot

Full source

theorem not_tendsto_atBot_of_tendsto_nhds (hf : Tendsto f l (𝓝 a)) : ¬Tendsto f l atBot :=
  hf.not_tendsto (disjoint_nhds_atBot a)

Non-convergence to Bottom Filter under Neighborhood Convergence

Informal description

Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property. If a function $f$ tends to a point $a$ in the neighborhood filter $\mathcal{N}(a)$, then $f$ does not tend to the filter `atBot` (the filter of sets containing all elements less than or equal to some element).

iSup_eq_of_forall_le_of_tendsto theorem

 {ι : Type*} {F : Filter ι} [Filter.NeBot F] [ConditionallyCompleteLattice α] [TopologicalSpace α] [ClosedIicTopology α]
  {a : α} {f : ι → α} (hle : ∀ i, f i ≤ a) (hlim : Filter.Tendsto f F (𝓝 a)) : ⨆ i, f i = a

Full source

theorem iSup_eq_of_forall_le_of_tendsto {ι : Type*} {F : Filter ι} [Filter.NeBot F]
    [ConditionallyCompleteLattice α] [TopologicalSpace α] [ClosedIicTopology α]
    {a : α} {f : ι → α} (hle : ∀ i, f i ≤ a) (hlim : Filter.Tendsto f F (𝓝 a)) :
    ⨆ i, f i = a :=
  have := F.nonempty_of_neBot
  (IsLUB.range_of_tendsto hle hlim).ciSup_eq

Supremum Equals Limit Under Bounded Convergence in Closed Lower Interval Topology

Informal description

Let $\alpha$ be a conditionally complete lattice equipped with a topology and the `ClosedIicTopology` property. Let $\iota$ be a type and $F$ be a non-trivial filter on $\iota$. For a function $f : \iota \to \alpha$ and an element $a \in \alpha$, if $f(i) \leq a$ for all $i \in \iota$ and $f$ tends to $a$ along $F$, then the supremum of $f$ over $\iota$ equals $a$, i.e., $\bigsqcup_{i} f(i) = a$.

iUnion_Iic_eq_Iio_of_lt_of_tendsto theorem

 {ι : Type*} {F : Filter ι} [F.NeBot] [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [ClosedIicTopology α]
  {a : α} {f : ι → α} (hlt : ∀ i, f i < a) (hlim : Tendsto f F (𝓝 a)) : ⋃ i : ι, Iic (f i) = Iio a

Full source

theorem iUnion_Iic_eq_Iio_of_lt_of_tendsto {ι : Type*} {F : Filter ι} [F.NeBot]
    [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [ClosedIicTopology α]
    {a : α} {f : ι → α} (hlt : ∀ i, f i < a) (hlim : Tendsto f F (𝓝 a)) :
    ⋃ i : ι, Iic (f i) = Iio a := by
  have obs : a ∉ range f := by
    rw [mem_range]
    rintro ⟨i, rfl⟩
    exact (hlt i).false
  rw [← biUnion_range, (IsLUB.range_of_tendsto (le_of_lt <| hlt ·) hlim).biUnion_Iic_eq_Iio obs]

Union of Lower Intervals Equals Open Lower Interval at Limit Point

Informal description

Let $\alpha$ be a conditionally complete linear order with a topology such that all lower intervals $(-\infty, a]$ are closed. Let $F$ be a non-trivial filter on an index set $\iota$, and let $f : \iota \to \alpha$ be a function such that $f(i) < a$ for all $i \in \iota$ and $f$ tends to $a$ along $F$. Then the union of the lower intervals $(-\infty, f(i)]$ for all $i \in \iota$ equals the open lower interval $(-\infty, a)$.

isOpen_Ioi theorem

: IsOpen (Ioi a)

Full source

theorem isOpen_Ioi : IsOpen (Ioi a) := by
  rw [← compl_Iic]
  exact isClosed_Iic.isOpen_compl

Openness of Left-Open Right-Infinite Interval in `ClosedIicTopology`

Informal description

For any element $a$ in a topological space $\alpha$ with a preorder and the `ClosedIicTopology` property, the left-open right-infinite interval $(a, \infty)$ (denoted as $\text{Ioi } a$) is an open set in the topology of $\alpha$.

interior_Ioi theorem

: interior (Ioi a) = Ioi a

Full source

@[simp]
theorem interior_Ioi : interior (Ioi a) = Ioi a :=
  isOpen_Ioi.interior_eq

Interior of Left-Open Right-Infinite Interval Equals Itself

Informal description

For any element $a$ in a topological space $\alpha$ with a preorder and the `ClosedIicTopology` property, the interior of the left-open right-infinite interval $(a, \infty)$ is equal to itself, i.e., $\text{interior}((a, \infty)) = (a, \infty)$.

Ioi_mem_nhds theorem

(h : a < b) : Ioi a ∈ 𝓝 b

Full source

theorem Ioi_mem_nhds (h : a < b) : IoiIoi a ∈ 𝓝 b := IsOpen.mem_nhds isOpen_Ioi h

Left-open interval is a neighborhood for larger points

Informal description

For any elements $a$ and $b$ in a topological space $\alpha$ with a preorder and the `ClosedIicTopology` property, if $a < b$, then the left-open right-infinite interval $(a, \infty)$ is a neighborhood of $b$.

eventually_gt_nhds theorem

(hab : b < a) : ∀ᶠ x in 𝓝 a, b < x

Full source

theorem eventually_gt_nhds (hab : b < a) : ∀ᶠ x in 𝓝 a, b < x := Ioi_mem_nhds hab

Eventual Strict Inequality in Neighborhoods for `ClosedIicTopology` Spaces

Informal description

For any elements $a$ and $b$ in a topological space $\alpha$ with a preorder and the `ClosedIicTopology` property, if $b < a$, then for all $x$ in some neighborhood of $a$, we have $b < x$.

eventually_ge_nhds theorem

(hab : b < a) : ∀ᶠ x in 𝓝 a, b ≤ x

Full source

theorem eventually_ge_nhds (hab : b < a) : ∀ᶠ x in 𝓝 a, b ≤ x := Ici_mem_nhds hab

Eventual Non-Strict Inequality in Neighborhoods for `ClosedIicTopology` Spaces

Informal description

For any elements $a$ and $b$ in a topological space $\alpha$ with a preorder and the `ClosedIicTopology` property, if $b < a$, then for all $x$ in some neighborhood of $a$, we have $b \leq x$.

Filter.Tendsto.eventually_const_lt theorem

{l : Filter γ} {f : γ → α} {u v : α} (hv : u < v) (h : Filter.Tendsto f l (𝓝 v)) : ∀ᶠ a in l, u < f a

Full source

theorem Filter.Tendsto.eventually_const_lt {l : Filter γ} {f : γ → α} {u v : α} (hv : u < v)
    (h : Filter.Tendsto f l (𝓝 v)) : ∀ᶠ a in l, u < f a :=
  h.eventually <| eventually_gt_nhds hv

Eventual Strict Inequality Under Tendsto in `ClosedIicTopology` Spaces

Informal description

Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property. For any filter $l$ on a type $\gamma$, any function $f : \gamma \to \alpha$, and any elements $u, v \in \alpha$ such that $u < v$, if $f$ tends to $v$ along $l$, then for eventually all $a$ in $l$, we have $u < f(a)$.

Filter.Tendsto.eventually_const_le theorem

{l : Filter γ} {f : γ → α} {u v : α} (hv : u < v) (h : Tendsto f l (𝓝 v)) : ∀ᶠ a in l, u ≤ f a

Full source

theorem Filter.Tendsto.eventually_const_le {l : Filter γ} {f : γ → α} {u v : α} (hv : u < v)
    (h : Tendsto f l (𝓝 v)) : ∀ᶠ a in l, u ≤ f a :=
  h.eventually <| eventually_ge_nhds hv

Eventual Non-Strict Inequality Under Tendsto in `ClosedIicTopology` Spaces

Informal description

Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property. For any filter $l$ on a type $\gamma$, any function $f : \gamma \to \alpha$, and any elements $u, v \in \alpha$ such that $u < v$, if $f$ tends to $v$ along $l$, then for eventually all $a$ in $l$, we have $u \leq f(a)$.

Dense.exists_gt theorem

[NoMaxOrder α] {s : Set α} (hs : Dense s) (x : α) : ∃ y ∈ s, x < y

Full source

protected theorem Dense.exists_gt [NoMaxOrder α] {s : Set α} (hs : Dense s) (x : α) :
    ∃ y ∈ s, x < y :=
  hs.exists_mem_open isOpen_Ioi (exists_gt x)

Existence of Greater Element in Dense Subset for Spaces without Maximal Elements

Informal description

Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property, and assume $\alpha$ has no maximal element (`NoMaxOrder`). For any dense subset $s$ of $\alpha$ and any element $x \in \alpha$, there exists an element $y \in s$ such that $x < y$.

Dense.exists_ge theorem

[NoMaxOrder α] {s : Set α} (hs : Dense s) (x : α) : ∃ y ∈ s, x ≤ y

Full source

protected theorem Dense.exists_ge [NoMaxOrder α] {s : Set α} (hs : Dense s) (x : α) :
    ∃ y ∈ s, x ≤ y :=
  (hs.exists_gt x).imp fun _ h ↦ ⟨h.1, h.2.le⟩

Existence of Greater or Equal Element in Dense Subset for Spaces without Maximal Elements

Informal description

Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property, and assume $\alpha$ has no maximal element. For any dense subset $s$ of $\alpha$ and any element $x \in \alpha$, there exists an element $y \in s$ such that $x \leq y$.

Dense.exists_ge' theorem

{s : Set α} (hs : Dense s) (htop : ∀ x, IsTop x → x ∈ s) (x : α) : ∃ y ∈ s, x ≤ y

Full source

theorem Dense.exists_ge' {s : Set α} (hs : Dense s) (htop : ∀ x, IsTop x → x ∈ s) (x : α) :
    ∃ y ∈ s, x ≤ y := by
  by_cases hx : IsTop x
  · exact ⟨x, htop x hx, le_rfl⟩
  · simp only [IsTop, not_forall, not_le] at hx
    rcases hs.exists_mem_open isOpen_Ioi hx with ⟨y, hys, hy : x < y⟩
    exact ⟨y, hys, hy.le⟩

Existence of Greater or Equal Element in Dense Subset Containing All Top Elements

Informal description

Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property. For any dense subset $s$ of $\alpha$ and any element $x \in \alpha$, if $s$ contains all top elements of $\alpha$ (i.e., for every $x$, if $x$ is a top element then $x \in s$), then there exists an element $y \in s$ such that $x \leq y$.

Ioo_mem_nhdsLT theorem

(H : a < b) : Ioo a b ∈ 𝓝[<] b

Full source

theorem Ioo_mem_nhdsLT (H : a < b) : IooIoo a b ∈ 𝓝[<] b := by
  simpa only [← Iio_inter_Ioi] using inter_mem_nhdsWithin _ (Ioi_mem_nhds H)

Open Interval is a Left-Neighborhood for Greater Points

Informal description

For any elements $a$ and $b$ in a topological space $\alpha$ with a preorder and the `ClosedIicTopology` property, if $a < b$, then the open interval $(a, b)$ is a neighborhood of $b$ in the left-neighborhood topology $\mathcal{N}_{[<]}(b)$.

Ioo_mem_nhdsLT_of_mem theorem

(H : b ∈ Ioc a c) : Ioo a c ∈ 𝓝[<] b

Full source

theorem Ioo_mem_nhdsLT_of_mem (H : b ∈ Ioc a c) : IooIoo a c ∈ 𝓝[<] b :=
  mem_of_superset (Ioo_mem_nhdsLT H.1) <| Ioo_subset_Ioo_right H.2

Open Interval is a Left-Neighborhood for Points in a Right-Closed Interval

Informal description

For any elements $a$, $b$, and $c$ in a topological space $\alpha$ with a preorder and the `ClosedIicTopology` property, if $b$ belongs to the left-open right-closed interval $(a, c]$, then the open interval $(a, c)$ is a neighborhood of $b$ in the left-neighborhood topology $\mathcal{N}_{[<]}(b)$.

CovBy.nhdsLT theorem

(h : a ⋖ b) : 𝓝[<] b = ⊥

Full source

protected theorem CovBy.nhdsLT (h : a ⋖ b) : 𝓝[<] b = ⊥ :=
  empty_mem_iff_bot.mp <| h.Ioo_eq ▸ Ioo_mem_nhdsLT h.1

Triviality of Left-Neighborhood Filter at a Covered Point

Informal description

For any elements $a$ and $b$ in a topological space $\alpha$ with a preorder and the `ClosedIicTopology` property, if $a$ is covered by $b$ (denoted $a \lessdot b$), then the left-neighborhood filter $\mathcal{N}_{[<]}(b)$ at $b$ is the trivial filter $\bot$.

PredOrder.nhdsLT theorem

[PredOrder α] : 𝓝[<] a = ⊥

Full source

protected theorem PredOrder.nhdsLT [PredOrder α] : 𝓝[<] a = ⊥ := by
  if h : IsMin a then simp [h.Iio_eq]
  else exact (Order.pred_covBy_of_not_isMin h).nhdsLT

Triviality of Left-Neighborhood Filter in PredOrder Topology

Informal description

In a topological space $\alpha$ with a preorder and a predecessor order structure (`PredOrder`), the left-neighborhood filter $\mathcal{N}_{[<]}(a)$ at any point $a \in \alpha$ is equal to the trivial filter $\bot$.

PredOrder.nhdsGT_eq_nhdsNE theorem

[PredOrder α] (a : α) : 𝓝[>] a = 𝓝[≠] a

Full source

theorem PredOrder.nhdsGT_eq_nhdsNE [PredOrder α] (a : α) : 𝓝[>] a = 𝓝[≠] a := by
  rw [← nhdsLT_sup_nhdsGT, PredOrder.nhdsLT, bot_sup_eq]

Right-Neighborhood Filter Equals Punctured Neighborhood Filter in PredOrder Topology

Informal description

In a topological space $\alpha$ with a predecessor order structure (`PredOrder`), the right-neighborhood filter $\mathcal{N}_{[>]}(a)$ at any point $a \in \alpha$ is equal to the punctured neighborhood filter $\mathcal{N}_{\neq}(a)$ (consisting of neighborhoods of $a$ excluding $a$ itself).

PredOrder.nhdsGE_eq_nhds theorem

[PredOrder α] (a : α) : 𝓝[≥] a = 𝓝 a

Full source

theorem PredOrder.nhdsGE_eq_nhds [PredOrder α] (a : α) : 𝓝[≥] a = 𝓝 a := by
  rw [← nhdsLT_sup_nhdsGE, PredOrder.nhdsLT, bot_sup_eq]

Right-Neighborhood Filter Equals Full Neighborhood Filter in PredOrder Topology

Informal description

In a topological space $\alpha$ with a predecessor order structure (`PredOrder`), the right-neighborhood filter $\mathcal{N}_{[\geq]}(a)$ at any point $a \in \alpha$ is equal to the full neighborhood filter $\mathcal{N}(a)$ of $a$.

Ico_mem_nhdsLT_of_mem theorem

(H : b ∈ Ioc a c) : Ico a c ∈ 𝓝[<] b

Full source

theorem Ico_mem_nhdsLT_of_mem (H : b ∈ Ioc a c) : IcoIco a c ∈ 𝓝[<] b :=
  mem_of_superset (Ioo_mem_nhdsLT_of_mem H) Ioo_subset_Ico_self

Left-Closed Right-Open Interval is a Left-Neighborhood for Points in a Right-Closed Interval

Informal description

For any elements $a$, $b$, and $c$ in a topological space $\alpha$ with a preorder and the `ClosedIicTopology` property, if $b$ belongs to the left-open right-closed interval $(a, c]$, then the left-closed right-open interval $[a, c)$ is a neighborhood of $b$ in the left-neighborhood topology $\mathcal{N}_{[<]}(b)$.

Ico_mem_nhdsLT theorem

(H : a < b) : Ico a b ∈ 𝓝[<] b

Full source

theorem Ico_mem_nhdsLT (H : a < b) : IcoIco a b ∈ 𝓝[<] b := Ico_mem_nhdsLT_of_mem ⟨H, le_rfl⟩

Left-neighborhood property of $[a,b)$ in `ClosedIicTopology` spaces

Informal description

For any elements $a$ and $b$ in a topological space $\alpha$ with a preorder and the `ClosedIicTopology` property, if $a < b$, then the left-closed right-open interval $[a, b)$ is a neighborhood of $b$ in the left-neighborhood topology $\mathcal{N}_{[<]}(b)$.

Ioc_mem_nhdsLT_of_mem theorem

(H : b ∈ Ioc a c) : Ioc a c ∈ 𝓝[<] b

Full source

theorem Ioc_mem_nhdsLT_of_mem (H : b ∈ Ioc a c) : IocIoc a c ∈ 𝓝[<] b :=
  mem_of_superset (Ioo_mem_nhdsLT_of_mem H) Ioo_subset_Ioc_self

Left-neighborhood property of right-closed intervals in `ClosedIicTopology` spaces

Informal description

For any elements $a$, $b$, and $c$ in a topological space $\alpha$ with a preorder and the `ClosedIicTopology` property, if $b$ belongs to the left-open right-closed interval $(a, c]$, then the interval $(a, c]$ is a neighborhood of $b$ in the left-neighborhood topology $\mathcal{N}_{[<]}(b)$.

Ioc_mem_nhdsLT theorem

(H : a < b) : Ioc a b ∈ 𝓝[<] b

Full source

theorem Ioc_mem_nhdsLT (H : a < b) : IocIoc a b ∈ 𝓝[<] b := Ioc_mem_nhdsLT_of_mem ⟨H, le_rfl⟩

Left-neighborhood property of right-closed intervals in `ClosedIicTopology` spaces for $a < b$

Informal description

Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property. For any elements $a, b \in \alpha$ such that $a < b$, the left-open right-closed interval $(a, b]$ is a neighborhood of $b$ in the left-neighborhood topology $\mathcal{N}_{[<]}(b)$.

Icc_mem_nhdsLT_of_mem theorem

(H : b ∈ Ioc a c) : Icc a c ∈ 𝓝[<] b

Full source

theorem Icc_mem_nhdsLT_of_mem (H : b ∈ Ioc a c) : IccIcc a c ∈ 𝓝[<] b :=
  mem_of_superset (Ioo_mem_nhdsLT_of_mem H) Ioo_subset_Icc_self

Closed Interval is a Left-Neighborhood for Points in Right-Closed Interval

Informal description

Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property. For any elements $a, b, c \in \alpha$ such that $b$ belongs to the left-open right-closed interval $(a, c]$, the closed interval $[a, c]$ is a neighborhood of $b$ in the left-neighborhood topology $\mathcal{N}_{[<]}(b)$.

Icc_mem_nhdsLT theorem

(H : a < b) : Icc a b ∈ 𝓝[<] b

Full source

theorem Icc_mem_nhdsLT (H : a < b) : IccIcc a b ∈ 𝓝[<] b := Icc_mem_nhdsLT_of_mem ⟨H, le_rfl⟩

Closed Interval is a Left-Neighborhood for Points in Strictly Increasing Order

Informal description

Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property. For any elements $a, b \in \alpha$ with $a < b$, the closed interval $[a, b]$ is a neighborhood of $b$ in the left-neighborhood topology $\mathcal{N}_{[<]}(b)$.

nhdsWithin_Ico_eq_nhdsLT theorem

(h : a < b) : 𝓝[Ico a b] b = 𝓝[<] b

Full source

@[simp]
theorem nhdsWithin_Ico_eq_nhdsLT (h : a < b) : 𝓝[Ico a b] b = 𝓝[<] b :=
  nhdsWithin_inter_of_mem <| nhdsWithin_le_nhds <| Ici_mem_nhds h

Equality of Left-Neighborhood Filters on Half-Open Interval $[a,b)$

Informal description

Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property. For any elements $a, b \in \alpha$ with $a < b$, the neighborhood filter of $b$ restricted to the interval $[a, b)$ is equal to the left-neighborhood filter of $b$ (i.e., $\mathcal{N}_{[a,b)}(b) = \mathcal{N}_{<}(b)$).

nhdsWithin_Ioo_eq_nhdsLT theorem

(h : a < b) : 𝓝[Ioo a b] b = 𝓝[<] b

Full source

@[simp]
theorem nhdsWithin_Ioo_eq_nhdsLT (h : a < b) : 𝓝[Ioo a b] b = 𝓝[<] b :=
  nhdsWithin_inter_of_mem <| nhdsWithin_le_nhds <| Ioi_mem_nhds h

Equality of Left-Neighborhood Filters on Open Interval

Informal description

For any elements $a$ and $b$ in a topological space $\alpha$ with a preorder and the `ClosedIicTopology` property, if $a < b$, then the neighborhood filter of $b$ restricted to the open interval $(a, b)$ is equal to the left-neighborhood filter of $b$ (i.e., the filter of neighborhoods to the left of $b$).

continuousWithinAt_Ico_iff_Iio theorem

(h : a < b) : ContinuousWithinAt f (Ico a b) b ↔ ContinuousWithinAt f (Iio b) b

Full source

@[simp]
theorem continuousWithinAt_Ico_iff_Iio (h : a < b) :
    ContinuousWithinAtContinuousWithinAt f (Ico a b) b ↔ ContinuousWithinAt f (Iio b) b := by
  simp only [ContinuousWithinAt, nhdsWithin_Ico_eq_nhdsLT h]

Equivalence of Continuity at Endpoint in Half-Open Interval vs Left-Infinite Interval

Informal description

Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property, and let $\beta$ be another topological space. For any elements $a, b \in \alpha$ with $a < b$, a function $f : \alpha \to \beta$ is continuous at $b$ within the interval $[a, b)$ if and only if it is continuous at $b$ within the interval $(-\infty, b)$.

continuousWithinAt_Ioo_iff_Iio theorem

(h : a < b) : ContinuousWithinAt f (Ioo a b) b ↔ ContinuousWithinAt f (Iio b) b

Full source

@[simp]
theorem continuousWithinAt_Ioo_iff_Iio (h : a < b) :
    ContinuousWithinAtContinuousWithinAt f (Ioo a b) b ↔ ContinuousWithinAt f (Iio b) b := by
  simp only [ContinuousWithinAt, nhdsWithin_Ioo_eq_nhdsLT h]

Equivalence of Continuity at Endpoint in Open Interval vs Left-Infinite Interval

Informal description

Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property. For any elements $a, b \in \alpha$ with $a < b$, a function $f : \alpha \to \beta$ is continuous at $b$ within the open interval $(a, b)$ if and only if it is continuous at $b$ within the left-infinite interval $(-\infty, b)$.

CovBy.nhdsLE theorem

(H : a ⋖ b) : 𝓝[≤] b = pure b

Full source

protected theorem CovBy.nhdsLE (H : a ⋖ b) : 𝓝[≤] b = pure b := by
  rw [← Iio_insert, nhdsWithin_insert, H.nhdsLT, sup_bot_eq]

Left-closed neighborhood filter at a covered point equals pure filter

Informal description

Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property. For any elements $a, b \in \alpha$ where $a$ is covered by $b$ (denoted $a \lessdot b$), the left-closed neighborhood filter at $b$ (denoted $\mathcal{N}[\leq] b$) equals the pure filter at $b$ (i.e., it contains exactly the sets that include $b$).

PredOrder.nhdsLE theorem

[PredOrder α] : 𝓝[≤] b = pure b

Full source

protected theorem PredOrder.nhdsLE [PredOrder α] : 𝓝[≤] b = pure b := by
  rw [← Iio_insert, nhdsWithin_insert, PredOrder.nhdsLT, sup_bot_eq]

Left-closed neighborhood filter equals pure filter in predecessor order topology

Informal description

In a topological space $\alpha$ with a preorder and a predecessor order structure (`PredOrder`), the left-closed neighborhood filter $\mathcal{N}[\leq] b$ at any point $b \in \alpha$ is equal to the pure filter at $b$, i.e., it contains exactly the sets that include $b$.

Ioc_mem_nhdsLE theorem

(H : a < b) : Ioc a b ∈ 𝓝[≤] b

Full source

theorem Ioc_mem_nhdsLE (H : a < b) : IocIoc a b ∈ 𝓝[≤] b :=
  inter_mem (nhdsWithin_le_nhds <| Ioi_mem_nhds H) self_mem_nhdsWithin

Left-open right-closed interval is a left-closed neighborhood for larger points

Informal description

For any elements $a$ and $b$ in a topological space $\alpha$ with a preorder and the `ClosedIicTopology` property, if $a < b$, then the left-open right-closed interval $(a, b]$ is a neighborhood of $b$ in the topology of left-closed neighborhoods $\mathcal{N}[\leq] b$.

Ioo_mem_nhdsLE_of_mem theorem

(H : b ∈ Ioo a c) : Ioo a c ∈ 𝓝[≤] b

Full source

theorem Ioo_mem_nhdsLE_of_mem (H : b ∈ Ioo a c) : IooIoo a c ∈ 𝓝[≤] b :=
  mem_of_superset (Ioc_mem_nhdsLE H.1) <| Ioc_subset_Ioo_right H.2

Open Interval is Left-Closed Neighborhood for Interior Points

Informal description

For any elements $a$, $b$, and $c$ in a topological space $\alpha$ with a preorder and the `ClosedIicTopology` property, if $b$ belongs to the open interval $(a, c)$, then $(a, c)$ is a neighborhood of $b$ in the topology of left-closed neighborhoods $\mathcal{N}[\leq] b$.

Ico_mem_nhdsLE_of_mem theorem

(H : b ∈ Ioo a c) : Ico a c ∈ 𝓝[≤] b

Full source

theorem Ico_mem_nhdsLE_of_mem (H : b ∈ Ioo a c) : IcoIco a c ∈ 𝓝[≤] b :=
  mem_of_superset (Ioo_mem_nhdsLE_of_mem H) Ioo_subset_Ico_self

Left-Closed Right-Open Interval as Left-Closed Neighborhood for Interior Points

Informal description

For any elements $a$, $b$, and $c$ in a topological space $\alpha$ with a preorder and the `ClosedIicTopology` property, if $b$ belongs to the open interval $(a, c)$, then the left-closed right-open interval $[a, c)$ is a neighborhood of $b$ in the topology of left-closed neighborhoods $\mathcal{N}[\leq] b$.

Ioc_mem_nhdsLE_of_mem theorem

(H : b ∈ Ioc a c) : Ioc a c ∈ 𝓝[≤] b

Full source

theorem Ioc_mem_nhdsLE_of_mem (H : b ∈ Ioc a c) : IocIoc a c ∈ 𝓝[≤] b :=
  mem_of_superset (Ioc_mem_nhdsLE H.1) <| Ioc_subset_Ioc_right H.2

Left-open right-closed interval is a left-closed neighborhood for interior points

Informal description

For any elements $a$, $b$, and $c$ in a topological space $\alpha$ with a preorder and the `ClosedIicTopology` property, if $b$ belongs to the left-open right-closed interval $(a, c]$, then $(a, c]$ is a neighborhood of $b$ in the topology of left-closed neighborhoods $\mathcal{N}[\leq] b$.

Icc_mem_nhdsLE_of_mem theorem

(H : b ∈ Ioc a c) : Icc a c ∈ 𝓝[≤] b

Full source

theorem Icc_mem_nhdsLE_of_mem (H : b ∈ Ioc a c) : IccIcc a c ∈ 𝓝[≤] b :=
  mem_of_superset (Ioc_mem_nhdsLE_of_mem H) Ioc_subset_Icc_self

Closed interval is a left-closed neighborhood for interior points of $(a, c]$

Informal description

Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property. For any elements $a, b, c \in \alpha$, if $b$ belongs to the left-open right-closed interval $(a, c]$, then the closed interval $[a, c]$ is a neighborhood of $b$ in the topology of left-closed neighborhoods $\mathcal{N}[\leq] b$.

Icc_mem_nhdsLE theorem

(H : a < b) : Icc a b ∈ 𝓝[≤] b

Full source

theorem Icc_mem_nhdsLE (H : a < b) : IccIcc a b ∈ 𝓝[≤] b := Icc_mem_nhdsLE_of_mem ⟨H, le_rfl⟩

Closed Interval as Left-Closed Neighborhood for Strictly Increasing Points

Informal description

Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property. For any elements $a, b \in \alpha$ with $a < b$, the closed interval $[a, b]$ is a neighborhood of $b$ in the topology of left-closed neighborhoods $\mathcal{N}[\leq] b$.

nhdsWithin_Icc_eq_nhdsLE theorem

(h : a < b) : 𝓝[Icc a b] b = 𝓝[≤] b

Full source

@[simp]
theorem nhdsWithin_Icc_eq_nhdsLE (h : a < b) : 𝓝[Icc a b] b = 𝓝[≤] b :=
  nhdsWithin_inter_of_mem <| nhdsWithin_le_nhds <| Ici_mem_nhds h

Equality of neighborhood filters within closed and left-infinite right-closed intervals

Informal description

Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property. For any elements $a, b \in \alpha$ with $a < b$, the neighborhood filter of $b$ within the closed interval $[a, b]$ is equal to the neighborhood filter of $b$ within the left-infinite right-closed interval $(-\infty, b]$.

nhdsWithin_Ioc_eq_nhdsLE theorem

(h : a < b) : 𝓝[Ioc a b] b = 𝓝[≤] b

Full source

@[simp]
theorem nhdsWithin_Ioc_eq_nhdsLE (h : a < b) : 𝓝[Ioc a b] b = 𝓝[≤] b :=
  nhdsWithin_inter_of_mem <| nhdsWithin_le_nhds <| Ioi_mem_nhds h

Equality of neighborhood filters within left-open right-closed and left-infinite right-closed intervals

Informal description

Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property. For any elements $a, b \in \alpha$ with $a < b$, the neighborhood filter of $b$ within the left-open right-closed interval $(a, b]$ is equal to the neighborhood filter of $b$ within the left-infinite right-closed interval $(-\infty, b]$.

continuousWithinAt_Icc_iff_Iic theorem

(h : a < b) : ContinuousWithinAt f (Icc a b) b ↔ ContinuousWithinAt f (Iic b) b

Full source

@[simp]
theorem continuousWithinAt_Icc_iff_Iic (h : a < b) :
    ContinuousWithinAtContinuousWithinAt f (Icc a b) b ↔ ContinuousWithinAt f (Iic b) b := by
  simp only [ContinuousWithinAt, nhdsWithin_Icc_eq_nhdsLE h]

Equivalence of Continuity at Right Endpoint in Closed and Left-Infinite Right-Closed Intervals

Informal description

Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property, and let $\beta$ be another topological space. For any elements $a, b \in \alpha$ with $a < b$ and any function $f : \alpha \to \beta$, the following are equivalent: 1. $f$ is continuous within the closed interval $[a, b]$ at the point $b$; 2. $f$ is continuous within the left-infinite right-closed interval $(-\infty, b]$ at the point $b$.

continuousWithinAt_Ioc_iff_Iic theorem

(h : a < b) : ContinuousWithinAt f (Ioc a b) b ↔ ContinuousWithinAt f (Iic b) b

Full source

@[simp]
theorem continuousWithinAt_Ioc_iff_Iic (h : a < b) :
    ContinuousWithinAtContinuousWithinAt f (Ioc a b) b ↔ ContinuousWithinAt f (Iic b) b := by
  simp only [ContinuousWithinAt, nhdsWithin_Ioc_eq_nhdsLE h]

Equivalence of Continuity at Right Endpoint in Left-Open and Left-Infinite Right-Closed Intervals

Informal description

Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property. For any elements $a, b \in \alpha$ with $a < b$ and any function $f : \alpha \to \beta$ (where $\beta$ is another topological space), the following are equivalent: 1. $f$ is continuous within the left-open right-closed interval $(a, b]$ at the point $b$; 2. $f$ is continuous within the left-infinite right-closed interval $(-\infty, b]$ at the point $b$.

isClosed_Ici theorem

{a : α} : IsClosed (Ici a)

Full source

theorem isClosed_Ici {a : α} : IsClosed (Ici a) :=
  ClosedIciTopology.isClosed_Ici a

Closedness of Upper Intervals in `ClosedIciTopology`

Informal description

For any element $a$ in a topological space $\alpha$ with a preorder and the `ClosedIciTopology` property, the closed interval $[a, \infty)$ is a closed set.

instClosedIicTopologyOrderDual instance

: ClosedIicTopology αᵒᵈ

Full source

instance : ClosedIicTopology αᵒᵈ where
  isClosed_Iic _ := isClosed_Ici (α := α)

Order Dual of Closed Lower Interval Topology is Closed Upper Interval Topology

Informal description

For any topological space $\alpha$ with a preorder, if $\alpha$ has the `ClosedIicTopology` property (where all lower intervals $(-\infty, a]$ are closed), then the order dual space $\alpha^{\text{op}}$ has the `ClosedIciTopology` property (where all upper intervals $[a, \infty)$ are closed).

closure_Ici theorem

(a : α) : closure (Ici a) = Ici a

Full source

@[simp]
theorem closure_Ici (a : α) : closure (Ici a) = Ici a :=
  isClosed_Ici.closure_eq

Closure of Upper Interval Equals Itself in `ClosedIciTopology`

Informal description

For any element $a$ in a topological space $\alpha$ with a preorder and the `ClosedIciTopology` property, the closure of the closed interval $[a, \infty)$ is equal to itself, i.e., $\text{closure}([a, \infty)) = [a, \infty)$.

ge_of_tendsto_of_frequently theorem

{x : Filter β} (lim : Tendsto f x (𝓝 a)) (h : ∃ᶠ c in x, b ≤ f c) : b ≤ a

Full source

lemma ge_of_tendsto_of_frequently {x : Filter β} (lim : Tendsto f x (𝓝 a))
    (h : ∃ᶠ c in x, b ≤ f c) : b ≤ a :=
  isClosed_Ici.mem_of_frequently_of_tendsto h lim

Inequality Preservation Under Frequent Lower Bounds and Convergence

Informal description

Let $f : \beta \to \alpha$ be a function from a type $\beta$ to a topological space $\alpha$ with a preorder and the `ClosedIciTopology` property. If $f$ tends to $a$ along a filter $x$ on $\beta$, and there exists a frequently occurring set of points $c$ in $x$ such that $b \leq f(c)$, then $b \leq a$.

ge_of_tendsto theorem

{x : Filter β} [NeBot x] (lim : Tendsto f x (𝓝 a)) (h : ∀ᶠ c in x, b ≤ f c) : b ≤ a

Full source

theorem ge_of_tendsto {x : Filter β} [NeBot x] (lim : Tendsto f x (𝓝 a))
    (h : ∀ᶠ c in x, b ≤ f c) : b ≤ a :=
  isClosed_Ici.mem_of_tendsto lim h

Inequality preservation under convergence with lower bounds in `ClosedIciTopology`

Informal description

Let $\alpha$ be a topological space with a preorder and the `ClosedIciTopology` property, and let $\beta$ be a type. Given a function $f : \beta \to \alpha$, a filter $x$ on $\beta$ that is not the trivial filter, and an element $b \in \alpha$, if $f$ converges to $a \in \alpha$ along $x$ and $b \leq f(c)$ holds for all $c$ in some eventually occurring subset of $x$, then $b \leq a$.

ge_of_tendsto' theorem

{x : Filter β} [NeBot x] (lim : Tendsto f x (𝓝 a)) (h : ∀ c, b ≤ f c) : b ≤ a

Full source

theorem ge_of_tendsto' {x : Filter β} [NeBot x] (lim : Tendsto f x (𝓝 a))
    (h : ∀ c, b ≤ f c) : b ≤ a :=
  ge_of_tendsto lim (Eventually.of_forall h)

Inequality preservation under convergence with uniform lower bounds in `ClosedIciTopology`

Informal description

Let $\alpha$ be a topological space with a preorder and the `ClosedIciTopology` property, and let $\beta$ be a type. Given a function $f : \beta \to \alpha$, a filter $x$ on $\beta$ that is not the trivial filter, and an element $b \in \alpha$, if $f$ converges to $a \in \alpha$ along $x$ and $b \leq f(c)$ holds for all $c \in \beta$, then $b \leq a$.

lowerBounds_closure theorem

(s : Set α) : lowerBounds (closure s : Set α) = lowerBounds s

Full source

@[simp] lemma lowerBounds_closure (s : Set α) : lowerBounds (closure s : Set α) = lowerBounds s :=
  ext fun a ↦ by simp_rw [mem_lowerBounds_iff_subset_Ici, isClosed_Ici.closure_subset_iff]

Equality of Lower Bounds for Closure in `ClosedIciTopology`

Informal description

For any subset $s$ of a topological space $\alpha$ with a preorder and the `ClosedIciTopology` property, the set of lower bounds of the closure of $s$ is equal to the set of lower bounds of $s$ itself. In other words, $\text{lowerBounds}(\overline{s}) = \text{lowerBounds}(s)$.

bddBelow_closure theorem

: BddBelow (closure s) ↔ BddBelow s

Full source

@[simp] lemma bddBelow_closure : BddBelowBddBelow (closure s) ↔ BddBelow s := by
  simp_rw [BddBelow, lowerBounds_closure]

Bounded Below Property of Closure in Closed Upper Interval Topology

Informal description

For any subset $s$ of a topological space $\alpha$ with a preorder and the `ClosedIciTopology` property, the closure of $s$ is bounded below if and only if $s$ itself is bounded below. In other words, $\overline{s}$ is bounded below $\iff$ $s$ is bounded below.

disjoint_nhds_atTop_iff theorem

: Disjoint (𝓝 a) atTop ↔ ¬IsTop a

Full source

@[simp]
theorem disjoint_nhds_atTop_iff : DisjointDisjoint (𝓝 a) atTop ↔ ¬IsTop a :=
  disjoint_nhds_atBot_iff (α := αᵒᵈ)

Disjointness of Neighborhood and Top Filters Characterizes Non-Top Elements

Informal description

For any element $a$ in a topological space $\alpha$ with a preorder and the `ClosedIciTopology` property, the neighborhood filter $\mathcal{N}(a)$ and the filter `atTop` (the filter of sets containing all elements greater than or equal to some element) are disjoint if and only if $a$ is not the greatest element in $\alpha$. In other words, $\mathcal{N}(a) \sqcap \text{atTop} = \bot \iff \neg (\text{IsTop } a)$.

IsGLB.range_of_tendsto theorem

{F : Filter β} [F.NeBot] (hle : ∀ i, a ≤ f i) (hlim : Tendsto f F (𝓝 a)) : IsGLB (range f) a

Full source

theorem IsGLB.range_of_tendsto {F : Filter β} [F.NeBot] (hle : ∀ i, a ≤ f i)
    (hlim : Tendsto f F (𝓝 a)) : IsGLB (range f) a :=
  IsLUB.range_of_tendsto (α := αᵒᵈ) hle hlim

Greatest lower bound property for limits of functions in closed upper interval topology

Informal description

Let $\alpha$ be a topological space with a preorder and the `ClosedIciTopology` property. Given a non-trivial filter $F$ on some type $\beta$, a function $f : \beta \to \alpha$, and an element $a \in \alpha$, if $a \leq f(i)$ for all $i \in \beta$ and $f$ tends to $a$ along $F$, then $a$ is the greatest lower bound of the range of $f$.

disjoint_nhds_atTop theorem

(a : α) : Disjoint (𝓝 a) atTop

Full source

theorem disjoint_nhds_atTop (a : α) : Disjoint (𝓝 a) atTop := disjoint_nhds_atBot (toDual a)

Disjointness of Neighborhood and Top Filters in Closed Upper Interval Topology

Informal description

For any element $a$ in a topological space $\alpha$ with a preorder and the `ClosedIciTopology` property, the neighborhood filter $\mathcal{N}(a)$ and the filter $\text{atTop}$ (the filter of sets containing all elements greater than or equal to some element) are disjoint.

inf_nhds_atTop theorem

(a : α) : 𝓝 a ⊓ atTop = ⊥

Full source

@[simp]
theorem inf_nhds_atTop (a : α) : 𝓝𝓝 a ⊓ atTop = ⊥ := (disjoint_nhds_atTop a).eq_bot

Infimum of Neighborhood and Top Filters is Bottom in Closed Upper Interval Topology

Informal description

For any element $a$ in a topological space $\alpha$ with a preorder and the `ClosedIciTopology` property, the infimum of the neighborhood filter $\mathcal{N}(a)$ and the filter $\text{atTop}$ (the filter of sets containing all elements greater than or equal to some element) is the bottom element $\bot$ of the filter lattice.

not_tendsto_nhds_of_tendsto_atTop theorem

(hf : Tendsto f l atTop) (a : α) : ¬Tendsto f l (𝓝 a)

Full source

theorem not_tendsto_nhds_of_tendsto_atTop (hf : Tendsto f l atTop) (a : α) : ¬Tendsto f l (𝓝 a) :=
  hf.not_tendsto (disjoint_nhds_atTop a).symm

Non-convergence to Neighborhoods for Functions Tending to Top Filter

Informal description

Let $\alpha$ be a topological space with a preorder and the `ClosedIciTopology` property. If a function $f$ tends to $\text{atTop}$ along a filter $l$, then $f$ does not tend to any neighborhood $\mathcal{N}(a)$ of a point $a \in \alpha$ along the same filter $l$.

not_tendsto_atTop_of_tendsto_nhds theorem

(hf : Tendsto f l (𝓝 a)) : ¬Tendsto f l atTop

Full source

theorem not_tendsto_atTop_of_tendsto_nhds (hf : Tendsto f l (𝓝 a)) : ¬Tendsto f l atTop :=
  hf.not_tendsto (disjoint_nhds_atTop a)

Non-convergence to atTop under neighborhood convergence in ClosedIciTopology

Informal description

Let $\alpha$ be a topological space with a preorder and the `ClosedIciTopology` property. If a function $f$ tends to a point $a$ in the neighborhood filter $\mathcal{N}(a)$, then $f$ does not tend to the filter $\text{atTop}$ (the filter of sets containing all elements greater than or equal to some element).

iInf_eq_of_forall_le_of_tendsto theorem

 {ι : Type*} {F : Filter ι} [F.NeBot] [ConditionallyCompleteLattice α] [TopologicalSpace α] [ClosedIciTopology α]
  {a : α} {f : ι → α} (hle : ∀ i, a ≤ f i) (hlim : Tendsto f F (𝓝 a)) : ⨅ i, f i = a

Full source

theorem iInf_eq_of_forall_le_of_tendsto {ι : Type*} {F : Filter ι} [F.NeBot]
    [ConditionallyCompleteLattice α] [TopologicalSpace α] [ClosedIciTopology α]
    {a : α} {f : ι → α} (hle : ∀ i, a ≤ f i) (hlim : Tendsto f F (𝓝 a)) :
    ⨅ i, f i = a :=
  iSup_eq_of_forall_le_of_tendsto (α := αᵒᵈ) hle hlim

Infimum Equals Limit Under Bounded Convergence in Closed Upper Interval Topology

Informal description

Let $\alpha$ be a conditionally complete lattice equipped with a topology satisfying the `ClosedIciTopology` property (i.e., all intervals $[a, \infty)$ are closed). Let $\iota$ be a type and $F$ be a non-trivial filter on $\iota$. For a function $f : \iota \to \alpha$ and an element $a \in \alpha$, if $a \leq f(i)$ for all $i \in \iota$ and $f$ tends to $a$ along $F$, then the infimum of $f$ over $\iota$ equals $a$, i.e., $\bigsqcap_{i} f(i) = a$.

iUnion_Ici_eq_Ioi_of_lt_of_tendsto theorem

 {ι : Type*} {F : Filter ι} [F.NeBot] [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [ClosedIciTopology α]
  {a : α} {f : ι → α} (hlt : ∀ i, a < f i) (hlim : Tendsto f F (𝓝 a)) : ⋃ i : ι, Ici (f i) = Ioi a

Full source

theorem iUnion_Ici_eq_Ioi_of_lt_of_tendsto {ι : Type*} {F : Filter ι} [F.NeBot]
    [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [ClosedIciTopology α]
    {a : α} {f : ι → α} (hlt : ∀ i, a < f i) (hlim : Tendsto f F (𝓝 a)) :
    ⋃ i : ι, Ici (f i) = Ioi a :=
  iUnion_Iic_eq_Iio_of_lt_of_tendsto (α := αᵒᵈ) hlt hlim

Union of Upper Intervals Equals Open Upper Interval at Limit Point

Informal description

Let $\alpha$ be a conditionally complete linear order equipped with a topology where all upper intervals $[a, \infty)$ are closed. Let $\iota$ be an index set, $F$ a non-trivial filter on $\iota$, and $f : \iota \to \alpha$ a function such that $a < f(i)$ for all $i \in \iota$ and $f$ converges to $a$ along $F$. Then the union of the upper intervals $[f(i), \infty)$ for all $i \in \iota$ equals the open upper interval $(a, \infty)$.

isOpen_Iio theorem

: IsOpen (Iio a)

Full source

theorem isOpen_Iio : IsOpen (Iio a) := isOpen_Ioi (α := αᵒᵈ)

Openness of Left-Infinite Right-Open Interval in Closed Upper Interval Topology

Informal description

For any element $a$ in a topological space $\alpha$ with a preorder and the `ClosedIciTopology` property, the left-infinite right-open interval $(-\infty, a)$ is an open set in the topology of $\alpha$.

interior_Iio theorem

: interior (Iio a) = Iio a

Full source

@[simp] theorem interior_Iio : interior (Iio a) = Iio a := isOpen_Iio.interior_eq

Interior of Left-Infinite Right-Open Interval Equals Itself

Informal description

For any element $a$ in a topological space $\alpha$ with a preorder and the `ClosedIciTopology` property, the interior of the left-infinite right-open interval $(-\infty, a)$ is equal to the interval itself, i.e., $\text{interior}((-\infty, a)) = (-\infty, a)$.

Iio_mem_nhds theorem

(h : a < b) : Iio b ∈ 𝓝 a

Full source

theorem Iio_mem_nhds (h : a < b) : IioIio b ∈ 𝓝 a := isOpen_Iio.mem_nhds h

Left-infinite interval $(-\infty, b)$ is a neighborhood of $a$ when $a < b$

Informal description

For any elements $a$ and $b$ in a topological space with a preorder, if $a < b$, then the left-infinite right-open interval $(-\infty, b)$ is a neighborhood of $a$.

eventually_lt_nhds theorem

(hab : a < b) : ∀ᶠ x in 𝓝 a, x < b

Full source

theorem eventually_lt_nhds (hab : a < b) : ∀ᶠ x in 𝓝 a, x < b := Iio_mem_nhds hab

Eventual Strict Inequality in Neighborhoods

Informal description

For any elements $a$ and $b$ in a topological space with a preorder, if $a < b$, then eventually for all $x$ in the neighborhood of $a$, we have $x < b$.

eventually_le_nhds theorem

(hab : a < b) : ∀ᶠ x in 𝓝 a, x ≤ b

Full source

theorem eventually_le_nhds (hab : a < b) : ∀ᶠ x in 𝓝 a, x ≤ b := Iic_mem_nhds hab

Eventual Non-Strict Inequality in Neighborhoods

Informal description

For any elements $a$ and $b$ in a topological space with a preorder, if $a < b$, then eventually for all $x$ in the neighborhood of $a$, we have $x \leq b$.

Filter.Tendsto.eventually_lt_const theorem

{l : Filter γ} {f : γ → α} {u v : α} (hv : v < u) (h : Filter.Tendsto f l (𝓝 v)) : ∀ᶠ a in l, f a < u

Full source

theorem Filter.Tendsto.eventually_lt_const {l : Filter γ} {f : γ → α} {u v : α} (hv : v < u)
    (h : Filter.Tendsto f l (𝓝 v)) : ∀ᶠ a in l, f a < u :=
  h.eventually <| eventually_lt_nhds hv

Eventual Strict Inequality for Functions Tending to a Limit in `ClosedIciTopology` Spaces

Informal description

Let $\alpha$ be a topological space with a preorder and the `ClosedIciTopology` property. Let $l$ be a filter on a type $\gamma$, and let $f : \gamma \to \alpha$ be a function. For any elements $u, v \in \alpha$ such that $v < u$, if $f$ tends to $v$ along the filter $l$, then eventually for all $a$ in $l$, we have $f(a) < u$.

Filter.Tendsto.eventually_le_const theorem

{l : Filter γ} {f : γ → α} {u v : α} (hv : v < u) (h : Tendsto f l (𝓝 v)) : ∀ᶠ a in l, f a ≤ u

Full source

theorem Filter.Tendsto.eventually_le_const {l : Filter γ} {f : γ → α} {u v : α} (hv : v < u)
    (h : Tendsto f l (𝓝 v)) : ∀ᶠ a in l, f a ≤ u :=
  h.eventually <| eventually_le_nhds hv

Eventual Non-Strict Inequality for Functions Tending to a Limit in `ClosedIciTopology` Spaces

Informal description

Let $\alpha$ be a topological space with a preorder and the `ClosedIciTopology` property. Let $l$ be a filter on a type $\gamma$, and let $f : \gamma \to \alpha$ be a function. For any elements $u, v \in \alpha$ such that $v < u$, if $f$ tends to $v$ along the filter $l$, then eventually for all $a$ in $l$, we have $f(a) \leq u$.

Dense.exists_lt theorem

[NoMinOrder α] {s : Set α} (hs : Dense s) (x : α) : ∃ y ∈ s, y < x

Full source

protected theorem Dense.exists_lt [NoMinOrder α] {s : Set α} (hs : Dense s) (x : α) :
    ∃ y ∈ s, y < x :=
  hs.orderDual.exists_gt x

Existence of Lesser Element in Dense Subset for Spaces without Minimal Elements

Informal description

Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property, and assume $\alpha$ has no minimal element (`NoMinOrder`). For any dense subset $s$ of $\alpha$ and any element $x \in \alpha$, there exists an element $y \in s$ such that $y < x$.

Dense.exists_le theorem

[NoMinOrder α] {s : Set α} (hs : Dense s) (x : α) : ∃ y ∈ s, y ≤ x

Full source

protected theorem Dense.exists_le [NoMinOrder α] {s : Set α} (hs : Dense s) (x : α) :
    ∃ y ∈ s, y ≤ x :=
  hs.orderDual.exists_ge x

Existence of a Less or Equal Element in Dense Subset for Spaces without Minimal Elements

Informal description

Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property, and assume $\alpha$ has no minimal element. For any dense subset $s$ of $\alpha$ and any element $x \in \alpha$, there exists an element $y \in s$ such that $y \leq x$.

Dense.exists_le' theorem

{s : Set α} (hs : Dense s) (hbot : ∀ x, IsBot x → x ∈ s) (x : α) : ∃ y ∈ s, y ≤ x

Full source

theorem Dense.exists_le' {s : Set α} (hs : Dense s) (hbot : ∀ x, IsBot x → x ∈ s) (x : α) :
    ∃ y ∈ s, y ≤ x :=
  hs.orderDual.exists_ge' hbot x

Existence of Less or Equal Element in Dense Subset Containing All Bottom Elements

Informal description

Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property. For any dense subset $s$ of $\alpha$ and any element $x \in \alpha$, if $s$ contains all bottom elements of $\alpha$ (i.e., for every $x$, if $x$ is a bottom element then $x \in s$), then there exists an element $y \in s$ such that $y \leq x$.

Ioo_mem_nhdsGT_of_mem theorem

(H : b ∈ Ico a c) : Ioo a c ∈ 𝓝[>] b

Full source

theorem Ioo_mem_nhdsGT_of_mem (H : b ∈ Ico a c) : IooIoo a c ∈ 𝓝[>] b :=
  mem_nhdsWithin.2
    ⟨Iio c, isOpen_Iio, H.2, by rw [inter_comm, Ioi_inter_Iio]; exact Ioo_subset_Ioo_left H.1⟩

Open Interval is Right Neighborhood for Points in Left-Closed Right-Open Interval

Informal description

For any elements $a, b, c$ in a preorder $\alpha$ with a topology satisfying `ClosedIciTopology`, if $b$ belongs to the left-closed right-open interval $[a, c)$, then the open interval $(a, c)$ is a neighborhood to the right of $b$ (i.e., $(a, c) \in \mathcal{N}_{>}(b)$).

Ioo_mem_nhdsGT theorem

(H : a < b) : Ioo a b ∈ 𝓝[>] a

Full source

theorem Ioo_mem_nhdsGT (H : a < b) : IooIoo a b ∈ 𝓝[>] a := Ioo_mem_nhdsGT_of_mem ⟨le_rfl, H⟩

Open Interval is Right Neighborhood for Strictly Greater Elements

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ with a topology satisfying `ClosedIciTopology`, if $a < b$, then the open interval $(a, b)$ is a neighborhood to the right of $a$ (i.e., $(a, b) \in \mathcal{N}_{>}(a)$).

SuccOrder.nhdsGT theorem

[SuccOrder α] : 𝓝[>] a = ⊥

Full source

protected theorem SuccOrder.nhdsGT [SuccOrder α] : 𝓝[>] a = ⊥ := PredOrder.nhdsLT (α := αᵒᵈ)

Triviality of Right-Neighborhood Filter in SuccOrder Topology

Informal description

In a topological space $\alpha$ with a successor order structure (`SuccOrder`), the right-neighborhood filter $\mathcal{N}_{[>]}(a)$ at any point $a \in \alpha$ is equal to the trivial filter $\bot$.

SuccOrder.nhdsLT_eq_nhdsNE theorem

[SuccOrder α] (a : α) : 𝓝[<] a = 𝓝[≠] a

Full source

theorem SuccOrder.nhdsLT_eq_nhdsNE [SuccOrder α] (a : α) : 𝓝[<] a = 𝓝[≠] a :=
  PredOrder.nhdsGT_eq_nhdsNE (α := αᵒᵈ) a

Left-Neighborhood Filter Equals Punctured Neighborhood Filter in SuccOrder Topology

Informal description

In a topological space $\alpha$ with a successor order structure (`SuccOrder`), the left-neighborhood filter $\mathcal{N}_{[<]}(a)$ at any point $a \in \alpha$ is equal to the punctured neighborhood filter $\mathcal{N}_{\neq}(a)$ (consisting of neighborhoods of $a$ excluding $a$ itself).

SuccOrder.nhdsLE_eq_nhds theorem

[SuccOrder α] (a : α) : 𝓝[≤] a = 𝓝 a

Full source

theorem SuccOrder.nhdsLE_eq_nhds [SuccOrder α] (a : α) : 𝓝[≤] a = 𝓝 a :=
  PredOrder.nhdsGE_eq_nhds (α := αᵒᵈ) a

Left-Neighborhood Filter Equals Full Neighborhood Filter in SuccOrder Topology

Informal description

In a topological space $\alpha$ with a successor order structure (`SuccOrder`), the left-neighborhood filter $\mathcal{N}_{[\leq]}(a)$ at any point $a \in \alpha$ is equal to the full neighborhood filter $\mathcal{N}(a)$ of $a$.

Ioc_mem_nhdsGT_of_mem theorem

(H : b ∈ Ico a c) : Ioc a c ∈ 𝓝[>] b

Full source

theorem Ioc_mem_nhdsGT_of_mem (H : b ∈ Ico a c) : IocIoc a c ∈ 𝓝[>] b :=
  mem_of_superset (Ioo_mem_nhdsGT_of_mem H) Ioo_subset_Ioc_self

Left-Open Right-Closed Interval is Right Neighborhood for Points in Left-Closed Right-Open Interval

Informal description

For any elements $a, b, c$ in a preorder $\alpha$ with a topology satisfying `ClosedIciTopology`, if $b$ belongs to the left-closed right-open interval $[a, c)$, then the left-open right-closed interval $(a, c]$ is a neighborhood to the right of $b$ (i.e., $(a, c] \in \mathcal{N}_{>}(b)$).

Ioc_mem_nhdsGT theorem

(H : a < b) : Ioc a b ∈ 𝓝[>] a

Full source

theorem Ioc_mem_nhdsGT (H : a < b) : IocIoc a b ∈ 𝓝[>] a := Ioc_mem_nhdsGT_of_mem ⟨le_rfl, H⟩

Right neighborhood property for left-open right-closed intervals

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ with a topology satisfying `ClosedIciTopology`, if $a < b$, then the left-open right-closed interval $(a, b]$ is a neighborhood to the right of $a$ (i.e., $(a, b] \in \mathcal{N}_{>}(a)$).

Ico_mem_nhdsGT_of_mem theorem

(H : b ∈ Ico a c) : Ico a c ∈ 𝓝[>] b

Full source

theorem Ico_mem_nhdsGT_of_mem (H : b ∈ Ico a c) : IcoIco a c ∈ 𝓝[>] b :=
  mem_of_superset (Ioo_mem_nhdsGT_of_mem H) Ioo_subset_Ico_self

Left-Closed Right-Open Interval is Right Neighborhood for Points in Itself

Informal description

For any elements $a, b, c$ in a preorder $\alpha$ with a topology satisfying `ClosedIciTopology`, if $b$ belongs to the left-closed right-open interval $[a, c)$, then the interval $[a, c)$ is a neighborhood to the right of $b$ (i.e., $[a, c) \in \mathcal{N}_{>}(b)$).

Ico_mem_nhdsGT theorem

(H : a < b) : Ico a b ∈ 𝓝[>] a

Full source

theorem Ico_mem_nhdsGT (H : a < b) : IcoIco a b ∈ 𝓝[>] a := Ico_mem_nhdsGT_of_mem ⟨le_rfl, H⟩

Left-Closed Right-Open Interval is Right Neighborhood for Strictly Increasing Points

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ with a topology satisfying `ClosedIciTopology`, if $a < b$, then the left-closed right-open interval $[a, b)$ is a neighborhood to the right of $a$ (i.e., $[a, b) \in \mathcal{N}_{>}(a)$).

Icc_mem_nhdsGT_of_mem theorem

(H : b ∈ Ico a c) : Icc a c ∈ 𝓝[>] b

Full source

theorem Icc_mem_nhdsGT_of_mem (H : b ∈ Ico a c) : IccIcc a c ∈ 𝓝[>] b :=
  mem_of_superset (Ioo_mem_nhdsGT_of_mem H) Ioo_subset_Icc_self

Closed Interval is Right Neighborhood for Points in Left-Closed Right-Open Interval

Informal description

For any elements $a, b, c$ in a preorder $\alpha$ with a topology satisfying `ClosedIciTopology`, if $b$ belongs to the left-closed right-open interval $[a, c)$, then the closed interval $[a, c]$ is a neighborhood to the right of $b$ (i.e., $[a, c] \in \mathcal{N}_{>}(b)$).

Icc_mem_nhdsGT theorem

(H : a < b) : Icc a b ∈ 𝓝[>] a

Full source

theorem Icc_mem_nhdsGT (H : a < b) : IccIcc a b ∈ 𝓝[>] a := Icc_mem_nhdsGT_of_mem ⟨le_rfl, H⟩

Closed Interval is Right Neighborhood for Strictly Increasing Points

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ with a topology satisfying `ClosedIciTopology`, if $a < b$, then the closed interval $[a, b]$ is a neighborhood to the right of $a$ (i.e., $[a, b] \in \mathcal{N}_{>}(a)$).

nhdsWithin_Ioc_eq_nhdsGT theorem

(h : a < b) : 𝓝[Ioc a b] a = 𝓝[>] a

Full source

@[simp]
theorem nhdsWithin_Ioc_eq_nhdsGT (h : a < b) : 𝓝[Ioc a b] a = 𝓝[>] a :=
  nhdsWithin_inter_of_mem' <| nhdsWithin_le_nhds <| Iic_mem_nhds h

Equality of Right-Neighborhood Filter and Left-Open Right-Closed Interval Neighborhood Filter at a Point

Informal description

For any elements $a$ and $b$ in a topological space $\alpha$ with a preorder, if $a < b$, then the neighborhood filter of $a$ restricted to the left-open right-closed interval $(a, b]$ is equal to the right-neighborhood filter of $a$ (i.e., $\mathcal{N}_{(a,b]}(a) = \mathcal{N}_{>a}$).

nhdsWithin_Ioo_eq_nhdsGT theorem

(h : a < b) : 𝓝[Ioo a b] a = 𝓝[>] a

Full source

@[simp]
theorem nhdsWithin_Ioo_eq_nhdsGT (h : a < b) : 𝓝[Ioo a b] a = 𝓝[>] a :=
  nhdsWithin_inter_of_mem' <| nhdsWithin_le_nhds <| Iio_mem_nhds h

Equality of Right-Neighborhood Filter and Open Interval Neighborhood Filter at a Point

Informal description

For any elements $a$ and $b$ in a topological space with a preorder, if $a < b$, then the neighborhood filter of $a$ restricted to the open interval $(a, b)$ is equal to the right-neighborhood filter of $a$ (i.e., the filter of neighborhoods to the right of $a$). In other words, $\mathcal{N}_{(a,b)}(a) = \mathcal{N}_{>a}$.

continuousWithinAt_Ioc_iff_Ioi theorem

(h : a < b) : ContinuousWithinAt f (Ioc a b) a ↔ ContinuousWithinAt f (Ioi a) a

Full source

@[simp]
theorem continuousWithinAt_Ioc_iff_Ioi (h : a < b) :
    ContinuousWithinAtContinuousWithinAt f (Ioc a b) a ↔ ContinuousWithinAt f (Ioi a) a := by
  simp only [ContinuousWithinAt, nhdsWithin_Ioc_eq_nhdsGT h]

Equivalence of Continuity at a Point in Right-Closed and Right-Infinite Intervals

Informal description

Let $a$ and $b$ be elements in a topological space with a preorder such that $a < b$. A function $f$ is continuous at $a$ within the left-open right-closed interval $(a, b]$ if and only if it is continuous at $a$ within the right-infinite interval $(a, \infty)$.

continuousWithinAt_Ioo_iff_Ioi theorem

(h : a < b) : ContinuousWithinAt f (Ioo a b) a ↔ ContinuousWithinAt f (Ioi a) a

Full source

@[simp]
theorem continuousWithinAt_Ioo_iff_Ioi (h : a < b) :
    ContinuousWithinAtContinuousWithinAt f (Ioo a b) a ↔ ContinuousWithinAt f (Ioi a) a := by
  simp only [ContinuousWithinAt, nhdsWithin_Ioo_eq_nhdsGT h]

Equivalence of Continuity at a Point in Open Interval and Right-Neighborhood

Informal description

For any two elements $a$ and $b$ in a topological space with a preorder, if $a < b$, then a function $f$ is continuous within the open interval $(a, b)$ at the point $a$ if and only if it is continuous within the right-neighborhood $(a, \infty)$ at $a$. In other words, $f$ is continuous at $a$ from the right within $(a, b)$ if and only if it is continuous at $a$ from the right within $(a, \infty)$.

Ico_mem_nhdsGE theorem

(H : a < b) : Ico a b ∈ 𝓝[≥] a

Full source

theorem Ico_mem_nhdsGE (H : a < b) : IcoIco a b ∈ 𝓝[≥] a :=
  inter_mem_nhdsWithin _ <| Iio_mem_nhds H

Left-closed right-open interval is a right-neighborhood for $a < b$

Informal description

For any elements $a$ and $b$ in a topological space with a preorder, if $a < b$, then the left-closed right-open interval $[a, b)$ is a neighborhood of $a$ in the right-neighborhood filter $\mathcal{N}_{\geq a}$.

Ico_mem_nhdsGE_of_mem theorem

(H : b ∈ Ico a c) : Ico a c ∈ 𝓝[≥] b

Full source

theorem Ico_mem_nhdsGE_of_mem (H : b ∈ Ico a c) : IcoIco a c ∈ 𝓝[≥] b :=
  mem_of_superset (Ico_mem_nhdsGE H.2) <| Ico_subset_Ico_left H.1

Membership in Left-Closed Right-Open Interval Implies Right-Neighborhood Property

Informal description

For any elements $a, b, c$ in a topological space $\alpha$ with a preorder and the `ClosedIciTopology` property, if $b$ belongs to the left-closed right-open interval $[a, c)$, then this interval is a neighborhood of $b$ in the right-neighborhood filter $\mathcal{N}_{\geq b}$.

Ioo_mem_nhdsGE_of_mem theorem

(H : b ∈ Ioo a c) : Ioo a c ∈ 𝓝[≥] b

Full source

theorem Ioo_mem_nhdsGE_of_mem (H : b ∈ Ioo a c) : IooIoo a c ∈ 𝓝[≥] b :=
  mem_of_superset (Ico_mem_nhdsGE H.2) <| Ico_subset_Ioo_left H.1

Open Interval is Right-Neighborhood for Points Within It

Informal description

For any elements $a, b, c$ in a topological space with a preorder, if $b$ belongs to the open interval $(a, c)$, then the open interval $(a, c)$ is a neighborhood of $b$ in the right-neighborhood filter $\mathcal{N}_{\geq b}$.

Ioc_mem_nhdsGE_of_mem theorem

(H : b ∈ Ioo a c) : Ioc a c ∈ 𝓝[≥] b

Full source

theorem Ioc_mem_nhdsGE_of_mem (H : b ∈ Ioo a c) : IocIoc a c ∈ 𝓝[≥] b :=
  mem_of_superset (Ioo_mem_nhdsGE_of_mem H) Ioo_subset_Ioc_self

Left-Open Right-Closed Interval is Right-Neighborhood for Points in Open Interval

Informal description

For any elements $a, b, c$ in a topological space $\alpha$ with a preorder and the `ClosedIciTopology` property, if $b$ belongs to the open interval $(a, c)$, then the left-open right-closed interval $(a, c]$ is a neighborhood of $b$ in the right-neighborhood filter $\mathcal{N}_{\geq b}$.

Icc_mem_nhdsGE_of_mem theorem

(H : b ∈ Ico a c) : Icc a c ∈ 𝓝[≥] b

Full source

theorem Icc_mem_nhdsGE_of_mem (H : b ∈ Ico a c) : IccIcc a c ∈ 𝓝[≥] b :=
  mem_of_superset (Ico_mem_nhdsGE_of_mem H) Ico_subset_Icc_self

Closed Interval is Right-Neighborhood for Points in Left-Closed Right-Open Interval

Informal description

For any elements $a, b, c$ in a topological space $\alpha$ with a preorder and the `ClosedIciTopology` property, if $b$ belongs to the left-closed right-open interval $[a, c)$, then the closed interval $[a, c]$ is a neighborhood of $b$ in the right-neighborhood filter $\mathcal{N}_{\geq b}$.

Icc_mem_nhdsGE theorem

(H : a < b) : Icc a b ∈ 𝓝[≥] a

Full source

theorem Icc_mem_nhdsGE (H : a < b) : IccIcc a b ∈ 𝓝[≥] a := Icc_mem_nhdsGE_of_mem ⟨le_rfl, H⟩

Closed Interval is Right-Neighborhood at Left Endpoint when $a < b$

Informal description

For any elements $a$ and $b$ in a topological space $\alpha$ with a preorder and the `ClosedIciTopology` property, if $a < b$, then the closed interval $[a, b]$ is a neighborhood of $a$ in the right-neighborhood filter $\mathcal{N}_{\geq a}$.

nhdsWithin_Icc_eq_nhdsGE theorem

(h : a < b) : 𝓝[Icc a b] a = 𝓝[≥] a

Full source

@[simp]
theorem nhdsWithin_Icc_eq_nhdsGE (h : a < b) : 𝓝[Icc a b] a = 𝓝[≥] a :=
  nhdsWithin_inter_of_mem' <| nhdsWithin_le_nhds <| Iic_mem_nhds h

Neighborhood equality for $[a, b]$ and $[a, \infty)$ at $a$ when $a < b$

Informal description

For any elements $a$ and $b$ in a topological space with a preorder, if $a < b$, then the neighborhood filter of $a$ restricted to the closed interval $[a, b]$ is equal to the neighborhood filter of $a$ restricted to the right-closed interval $[a, \infty)$. In other words, $\mathcal{N}_{[a, b]}(a) = \mathcal{N}_{[a, \infty)}(a)$ whenever $a < b$.

nhdsWithin_Ico_eq_nhdsGE theorem

(h : a < b) : 𝓝[Ico a b] a = 𝓝[≥] a

Full source

@[simp]
theorem nhdsWithin_Ico_eq_nhdsGE (h : a < b) : 𝓝[Ico a b] a = 𝓝[≥] a :=
  nhdsWithin_inter_of_mem' <| nhdsWithin_le_nhds <| Iio_mem_nhds h

Neighborhood equality for $[a, b)$ and $[a, \infty)$ at $a$ when $a < b$

Informal description

For any elements $a$ and $b$ in a topological space with a preorder, if $a < b$, then the neighborhood filter of $a$ restricted to the left-closed right-open interval $[a, b)$ is equal to the neighborhood filter of $a$ restricted to the right-closed interval $[a, \infty)$. In other words, $\mathcal{N}_{[a, b)}(a) = \mathcal{N}_{[a, \infty)}(a)$ whenever $a < b$.

continuousWithinAt_Icc_iff_Ici theorem

(h : a < b) : ContinuousWithinAt f (Icc a b) a ↔ ContinuousWithinAt f (Ici a) a

Full source

@[simp]
theorem continuousWithinAt_Icc_iff_Ici (h : a < b) :
    ContinuousWithinAtContinuousWithinAt f (Icc a b) a ↔ ContinuousWithinAt f (Ici a) a := by
  simp only [ContinuousWithinAt, nhdsWithin_Icc_eq_nhdsGE h]

Equivalence of Continuity in $[a, b]$ and $[a, \infty)$ at $a$ when $a < b$

Informal description

Let $\alpha$ be a topological space with a preorder and the `ClosedIciTopology` property. For any two elements $a, b \in \alpha$ with $a < b$, a function $f : \alpha \to \beta$ is continuous at $a$ within the closed interval $[a, b]$ if and only if it is continuous at $a$ within the right-closed interval $[a, \infty)$. In other words, the continuity of $f$ at $a$ from the right in the closed interval $[a, b]$ is equivalent to its continuity at $a$ from the right in the right-closed interval $[a, \infty)$.

continuousWithinAt_Ico_iff_Ici theorem

(h : a < b) : ContinuousWithinAt f (Ico a b) a ↔ ContinuousWithinAt f (Ici a) a

Full source

@[simp]
theorem continuousWithinAt_Ico_iff_Ici (h : a < b) :
    ContinuousWithinAtContinuousWithinAt f (Ico a b) a ↔ ContinuousWithinAt f (Ici a) a := by
  simp only [ContinuousWithinAt, nhdsWithin_Ico_eq_nhdsGE h]

Equivalence of Continuity in $[a, b)$ and $[a, \infty)$ at $a$ when $a < b$

Informal description

Let $\alpha$ be a topological space with a preorder and the `ClosedIciTopology` property. For any two elements $a, b \in \alpha$ with $a < b$, a function $f : \alpha \to \beta$ is continuous at $a$ within the interval $[a, b)$ if and only if it is continuous at $a$ within the interval $[a, \infty)$. In other words, the continuity of $f$ at $a$ from the right in the left-closed right-open interval $[a, b)$ is equivalent to its continuity at $a$ from the right in the left-closed right-infinite interval $[a, \infty)$.

Subtype.instOrderClosedTopology instance

{p : α → Prop} : OrderClosedTopology (Subtype p)

Full source

instance {p : α → Prop} : OrderClosedTopology (Subtype p) :=
  have this : Continuous fun p : SubtypeSubtype p × Subtype p => ((p.fst : α), (p.snd : α)) :=
    continuous_subtype_val.prodMap continuous_subtype_val
  OrderClosedTopology.mk (t.isClosed_le'.preimage this)

Order-Closed Topology on Subsets

Informal description

For any subset of a preorder with an order-closed topology, the induced topology on the subset is also order-closed.

isClosed_le_prod theorem

: IsClosed {p : α × α | p.1 ≤ p.2}

Full source

theorem isClosed_le_prod : IsClosed { p : α × α | p.1 ≤ p.2 } :=
  t.isClosed_le'

Closedness of the Order Relation in Product Space

Informal description

In a topological space $\alpha$ equipped with a preorder and an order-closed topology, the set $\{(x, y) \in \alpha \times \alpha \mid x \leq y\}$ is closed in the product topology.

isClosed_le theorem

[TopologicalSpace β] {f g : β → α} (hf : Continuous f) (hg : Continuous g) : IsClosed {b | f b ≤ g b}

Full source

theorem isClosed_le [TopologicalSpace β] {f g : β → α} (hf : Continuous f) (hg : Continuous g) :
    IsClosed { b | f b ≤ g b } :=
  continuous_iff_isClosed.mp (hf.prodMk hg) _ isClosed_le_prod

Closedness of the Sublevel Set under Continuous Functions

Informal description

Let $\alpha$ be a topological space with a preorder and an order-closed topology, and let $\beta$ be another topological space. For any continuous functions $f, g \colon \beta \to \alpha$, the set $\{b \in \beta \mid f(b) \leq g(b)\}$ is closed in $\beta$.

instClosedIicTopology instance

: ClosedIicTopology α

Full source

instance : ClosedIicTopology α where
  isClosed_Iic _ := isClosed_le continuous_id continuous_const

Closed Lower Interval Topology Property

Informal description

For any topological space $\alpha$ with a preorder, the topology satisfies the `ClosedIicTopology` property if for every element $a \in \alpha$, the lower interval $(-\infty, a]$ is a closed set in the topology.

instClosedIciTopology instance

: ClosedIciTopology α

Full source

instance : ClosedIciTopology α where
  isClosed_Ici _ := isClosed_le continuous_const continuous_id

Closed Upper Interval Topology Property

Informal description

For any topological space $\alpha$ with a preorder, the topology satisfies the `ClosedIciTopology` property if for every element $a \in \alpha$, the closed interval $[a, +\infty)$ is a closed set in the topology.

instOrderClosedTopologyOrderDual instance

: OrderClosedTopology αᵒᵈ

Full source

instance : OrderClosedTopology αᵒᵈ :=
  ⟨(OrderClosedTopology.isClosed_le' (α := α)).preimage continuous_swap⟩

Order-Closed Topology on Dual Order

Informal description

For any preorder $\alpha$ with an order-closed topology, the dual order $\alpha^{\text{op}}$ also has an order-closed topology.

isClosed_Icc theorem

{a b : α} : IsClosed (Icc a b)

Full source

theorem isClosed_Icc {a b : α} : IsClosed (Icc a b) :=
  IsClosed.inter isClosed_Ici isClosed_Iic

Closedness of Closed Intervals in Order-Closed Topology

Informal description

For any elements $a$ and $b$ in a topological space $\alpha$ with a preorder and order-closed topology, the closed interval $[a, b] = \{x \in \alpha \mid a \leq x \leq b\}$ is a closed set.

closure_Icc theorem

(a b : α) : closure (Icc a b) = Icc a b

Full source

@[simp]
theorem closure_Icc (a b : α) : closure (Icc a b) = Icc a b :=
  isClosed_Icc.closure_eq

Closure of Closed Interval Equals Itself in Order-Closed Topology

Informal description

For any elements $a$ and $b$ in a topological space $\alpha$ with a preorder and order-closed topology, the closure of the closed interval $[a, b] = \{x \in \alpha \mid a \leq x \leq b\}$ is equal to the interval itself.

le_of_tendsto_of_tendsto theorem

 {f g : β → α} {b : Filter β} {a₁ a₂ : α} [NeBot b] (hf : Tendsto f b (𝓝 a₁)) (hg : Tendsto g b (𝓝 a₂))
  (h : f ≤ᶠ[b] g) : a₁ ≤ a₂

Full source

theorem le_of_tendsto_of_tendsto {f g : β → α} {b : Filter β} {a₁ a₂ : α} [NeBot b]
    (hf : Tendsto f b (𝓝 a₁)) (hg : Tendsto g b (𝓝 a₂)) (h : f ≤ᶠ[b] g) : a₁ ≤ a₂ :=
  have : Tendsto (fun b => (f b, g b)) b (𝓝 (a₁, a₂)) := hf.prodMk_nhds hg
  show (a₁, a₂)(a₁, a₂) ∈ { p : α × α | p.1 ≤ p.2 } from t.isClosed_le'.mem_of_tendsto this h

Limit Inequality Preservation in Order-Closed Topology

Informal description

Let $\alpha$ be a topological space with a preorder and order-closed topology. Let $f, g : \beta \to \alpha$ be functions and $b$ a non-trivial filter on $\beta$. If $f$ converges to $a_1$ along $b$, $g$ converges to $a_2$ along $b$, and $f(x) \leq g(x)$ for all $x$ in a set belonging to $b$, then $a_1 \leq a_2$.

le_of_tendsto_of_tendsto' theorem

 {f g : β → α} {b : Filter β} {a₁ a₂ : α} [NeBot b] (hf : Tendsto f b (𝓝 a₁)) (hg : Tendsto g b (𝓝 a₂))
  (h : ∀ x, f x ≤ g x) : a₁ ≤ a₂

Full source

theorem le_of_tendsto_of_tendsto' {f g : β → α} {b : Filter β} {a₁ a₂ : α} [NeBot b]
    (hf : Tendsto f b (𝓝 a₁)) (hg : Tendsto g b (𝓝 a₂)) (h : ∀ x, f x ≤ g x) : a₁ ≤ a₂ :=
  le_of_tendsto_of_tendsto hf hg (Eventually.of_forall h)

Limit Inequality Preservation in Order-Closed Topology (Uniform Version)

Informal description

Let $\alpha$ be a topological space with a preorder and order-closed topology. Let $f, g : \beta \to \alpha$ be functions and $b$ a non-trivial filter on $\beta$. If $f$ converges to $a_1$ along $b$, $g$ converges to $a_2$ along $b$, and $f(x) \leq g(x)$ for all $x \in \beta$, then $a_1 \leq a_2$.

closure_le_eq theorem

 [TopologicalSpace β] {f g : β → α} (hf : Continuous f) (hg : Continuous g) : closure {b | f b ≤ g b} = {b | f b ≤ g b}

Full source

@[simp]
theorem closure_le_eq [TopologicalSpace β] {f g : β → α} (hf : Continuous f) (hg : Continuous g) :
    closure { b | f b ≤ g b } = { b | f b ≤ g b } :=
  (isClosed_le hf hg).closure_eq

Closure of Sublevel Set Equals Itself for Continuous Functions

Informal description

Let $\alpha$ be a topological space with a preorder and order-closed topology, and let $\beta$ be another topological space. For any continuous functions $f, g \colon \beta \to \alpha$, the closure of the set $\{b \in \beta \mid f(b) \leq g(b)\}$ is equal to the set itself. In other words, the sublevel set $\{b \mid f(b) \leq g(b)\}$ is closed in $\beta$.

closure_lt_subset_le theorem

 [TopologicalSpace β] {f g : β → α} (hf : Continuous f) (hg : Continuous g) : closure {b | f b < g b} ⊆ {b | f b ≤ g b}

Full source

theorem closure_lt_subset_le [TopologicalSpace β] {f g : β → α} (hf : Continuous f)
    (hg : Continuous g) : closureclosure { b | f b < g b } ⊆ { b | f b ≤ g b } :=
  (closure_minimal fun _ => le_of_lt) <| isClosed_le hf hg

Closure of Strict Sublevel Set Contained in Non-Strict Sublevel Set for Continuous Functions

Informal description

Let $\alpha$ be a topological space with a preorder and order-closed topology, and let $\beta$ be another topological space. For any continuous functions $f, g \colon \beta \to \alpha$, the closure of the set $\{b \in \beta \mid f(b) < g(b)\}$ is contained in the set $\{b \in \beta \mid f(b) \leq g(b)\}$.

ContinuousWithinAt.closure_le theorem

 [TopologicalSpace β] {f g : β → α} {s : Set β} {x : β} (hx : x ∈ closure s) (hf : ContinuousWithinAt f s x)
  (hg : ContinuousWithinAt g s x) (h : ∀ y ∈ s, f y ≤ g y) : f x ≤ g x

Full source

theorem ContinuousWithinAt.closure_le [TopologicalSpace β] {f g : β → α} {s : Set β} {x : β}
    (hx : x ∈ closure s) (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x)
    (h : ∀ y ∈ s, f y ≤ g y) : f x ≤ g x :=
  show (f x, g x)(f x, g x) ∈ { p : α × α | p.1 ≤ p.2 } from
    OrderClosedTopology.isClosed_le'.closure_subset ((hf.prodMk hg).mem_closure hx h)

Preservation of Inequality under Continuity at a Limit Point

Informal description

Let $X$ and $Y$ be topological spaces, where $Y$ is equipped with an order-closed topology. Let $s \subseteq X$ be a subset, and let $f, g: X \to Y$ be functions that are continuous within $s$ at a point $x \in \overline{s}$. If $f(y) \leq g(y)$ for all $y \in s$, then $f(x) \leq g(x)$.

IsClosed.isClosed_le theorem

 [TopologicalSpace β] {f g : β → α} {s : Set β} (hs : IsClosed s) (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
  IsClosed ({x ∈ s | f x ≤ g x})

Full source

/-- If `s` is a closed set and two functions `f` and `g` are continuous on `s`,
then the set `{x ∈ s | f x ≤ g x}` is a closed set. -/
theorem IsClosed.isClosed_le [TopologicalSpace β] {f g : β → α} {s : Set β} (hs : IsClosed s)
    (hf : ContinuousOn f s) (hg : ContinuousOn g s) : IsClosed ({ x ∈ s | f x ≤ g x }) :=
  (hf.prodMk hg).preimage_isClosed_of_isClosed hs OrderClosedTopology.isClosed_le'

Closedness of Sublevel Set under Continuous Functions

Informal description

Let $X$ and $Y$ be topological spaces, with $Y$ equipped with an order-closed topology. Let $s \subseteq X$ be a closed subset, and let $f, g: X \to Y$ be continuous functions when restricted to $s$. Then the set $\{x \in s \mid f(x) \leq g(x)\}$ is closed in $X$.

le_on_closure theorem

 [TopologicalSpace β] {f g : β → α} {s : Set β} (h : ∀ x ∈ s, f x ≤ g x) (hf : ContinuousOn f (closure s))
  (hg : ContinuousOn g (closure s)) ⦃x⦄ (hx : x ∈ closure s) : f x ≤ g x

Full source

theorem le_on_closure [TopologicalSpace β] {f g : β → α} {s : Set β} (h : ∀ x ∈ s, f x ≤ g x)
    (hf : ContinuousOn f (closure s)) (hg : ContinuousOn g (closure s)) ⦃x⦄ (hx : x ∈ closure s) :
    f x ≤ g x :=
  have : s ⊆ { y ∈ closure s | f y ≤ g y } := fun y hy => ⟨subset_closure hy, h y hy⟩
  (closure_minimal this (isClosed_closure.isClosed_le hf hg) hx).2

Inequality Preservation on Closure under Continuous Functions

Informal description

Let $X$ and $Y$ be topological spaces, where $Y$ is equipped with an order-closed topology. Let $s \subseteq X$ be a subset, and let $f, g: X \to Y$ be continuous functions on the closure of $s$. If $f(x) \leq g(x)$ for all $x \in s$, then $f(x) \leq g(x)$ for all $x$ in the closure of $s$.

IsClosed.epigraph theorem

 [TopologicalSpace β] {f : β → α} {s : Set β} (hs : IsClosed s) (hf : ContinuousOn f s) :
  IsClosed {p : β × α | p.1 ∈ s ∧ f p.1 ≤ p.2}

Full source

theorem IsClosed.epigraph [TopologicalSpace β] {f : β → α} {s : Set β} (hs : IsClosed s)
    (hf : ContinuousOn f s) : IsClosed { p : β × α | p.1 ∈ s ∧ f p.1 ≤ p.2 } :=
  (hs.preimage continuous_fst).isClosed_le (hf.comp continuousOn_fst Subset.rfl) continuousOn_snd

Closedness of Epigraph under Continuous Function

Informal description

Let $X$ and $Y$ be topological spaces, where $Y$ is equipped with an order-closed topology. Let $s \subseteq X$ be a closed subset, and let $f: X \to Y$ be a continuous function when restricted to $s$. Then the epigraph of $f$ over $s$, defined as the set $\{(x, y) \in X \times Y \mid x \in s \text{ and } f(x) \leq y\}$, is closed in the product space $X \times Y$.

IsClosed.hypograph theorem

 [TopologicalSpace β] {f : β → α} {s : Set β} (hs : IsClosed s) (hf : ContinuousOn f s) :
  IsClosed {p : β × α | p.1 ∈ s ∧ p.2 ≤ f p.1}

Full source

theorem IsClosed.hypograph [TopologicalSpace β] {f : β → α} {s : Set β} (hs : IsClosed s)
    (hf : ContinuousOn f s) : IsClosed { p : β × α | p.1 ∈ s ∧ p.2 ≤ f p.1 } :=
  (hs.preimage continuous_fst).isClosed_le continuousOn_snd (hf.comp continuousOn_fst Subset.rfl)

Closedness of Hypograph under Continuous Function

Informal description

Let $X$ and $Y$ be topological spaces, where $Y$ is equipped with an order-closed topology. Let $s \subseteq X$ be a closed subset, and let $f: X \to Y$ be a continuous function when restricted to $s$. Then the hypograph of $f$ over $s$, defined as the set $\{(x, y) \in X \times Y \mid x \in s \text{ and } y \leq f(x)\}$, is closed in the product space $X \times Y$.

OrderClosedTopology.to_t2Space instance

: T2Space α

Full source

instance (priority := 90) OrderClosedTopology.to_t2Space : T2Space α :=
  t2_iff_isClosed_diagonal.2 <| by
    simpa only [diagonal, le_antisymm_iff] using
      t.isClosed_le'.inter (isClosed_le continuous_snd continuous_fst)

Order-Closed Topologies are Hausdorff

Informal description

Every topological space with an order-closed topology is a Hausdorff space.

isOpen_lt theorem

[TopologicalSpace β] {f g : β → α} (hf : Continuous f) (hg : Continuous g) : IsOpen {b | f b < g b}

Full source

theorem isOpen_lt [TopologicalSpace β] {f g : β → α} (hf : Continuous f) (hg : Continuous g) :
    IsOpen { b | f b < g b } := by
  simpa only [lt_iff_not_le] using (isClosed_le hg hf).isOpen_compl

Openness of the Strict Sublevel Set under Continuous Functions

Informal description

Let $\alpha$ be a topological space with a preorder and an order-closed topology, and let $\beta$ be another topological space. For any continuous functions $f, g \colon \beta \to \alpha$, the set $\{b \in \beta \mid f(b) < g(b)\}$ is open in $\beta$.

isOpen_lt_prod theorem

: IsOpen {p : α × α | p.1 < p.2}

Full source

theorem isOpen_lt_prod : IsOpen { p : α × α | p.1 < p.2 } :=
  isOpen_lt continuous_fst continuous_snd

Openness of the Strict Order Relation in Product Space

Informal description

Let $\alpha$ be a topological space with a preorder and an order-closed topology. The set $\{(x, y) \in \alpha \times \alpha \mid x < y\}$ is open in the product topology on $\alpha \times \alpha$.

isOpen_Ioo theorem

: IsOpen (Ioo a b)

Full source

theorem isOpen_Ioo : IsOpen (Ioo a b) :=
  IsOpen.inter isOpen_Ioi isOpen_Iio

Openness of Open Intervals in Order-Closed Topology

Informal description

For any two elements $a$ and $b$ in a topological space $\alpha$ with a preorder and an order-closed topology, the open interval $(a, b) = \{x \in \alpha \mid a < x < b\}$ is an open set in the topology of $\alpha$.

interior_Ioo theorem

: interior (Ioo a b) = Ioo a b

Full source

@[simp]
theorem interior_Ioo : interior (Ioo a b) = Ioo a b :=
  isOpen_Ioo.interior_eq

Interior of Open Interval Equals Itself in Order-Closed Topology

Informal description

For any two elements $a$ and $b$ in a topological space $\alpha$ with a preorder and an order-closed topology, the interior of the open interval $(a, b) = \{x \in \alpha \mid a < x < b\}$ is equal to the interval itself, i.e., $\text{interior}((a, b)) = (a, b)$.

Ioo_subset_closure_interior theorem

: Ioo a b ⊆ closure (interior (Ioo a b))

Full source

theorem Ioo_subset_closure_interior : IooIoo a b ⊆ closure (interior (Ioo a b)) := by
  simp only [interior_Ioo, subset_closure]

Open Interval is Contained in Closure of Its Interior in Order-Closed Topology

Informal description

For any two elements $a$ and $b$ in a topological space $\alpha$ with a preorder and an order-closed topology, the open interval $(a, b) = \{x \in \alpha \mid a < x < b\}$ is contained in the closure of its interior, i.e., $(a, b) \subseteq \overline{\text{interior}((a, b))}$.

Ioo_mem_nhds theorem

{a b x : α} (ha : a < x) (hb : x < b) : Ioo a b ∈ 𝓝 x

Full source

theorem Ioo_mem_nhds {a b x : α} (ha : a < x) (hb : x < b) : IooIoo a b ∈ 𝓝 x :=
  IsOpen.mem_nhds isOpen_Ioo ⟨ha, hb⟩

Open Interval is a Neighborhood in Order-Closed Topology

Informal description

For any elements $a$, $b$, and $x$ in a topological space $\alpha$ with a preorder and an order-closed topology, if $a < x < b$, then the open interval $(a, b)$ is a neighborhood of $x$.

Ioc_mem_nhds theorem

{a b x : α} (ha : a < x) (hb : x < b) : Ioc a b ∈ 𝓝 x

Full source

theorem Ioc_mem_nhds {a b x : α} (ha : a < x) (hb : x < b) : IocIoc a b ∈ 𝓝 x :=
  mem_of_superset (Ioo_mem_nhds ha hb) Ioo_subset_Ioc_self

Left-Open Right-Closed Interval is a Neighborhood in Order-Closed Topology

Informal description

For any elements $a$, $b$, and $x$ in a topological space $\alpha$ with a preorder and an order-closed topology, if $a < x < b$, then the left-open right-closed interval $(a, b]$ is a neighborhood of $x$.

Ico_mem_nhds theorem

{a b x : α} (ha : a < x) (hb : x < b) : Ico a b ∈ 𝓝 x

Full source

theorem Ico_mem_nhds {a b x : α} (ha : a < x) (hb : x < b) : IcoIco a b ∈ 𝓝 x :=
  mem_of_superset (Ioo_mem_nhds ha hb) Ioo_subset_Ico_self

Left-Closed Right-Open Interval is a Neighborhood in Order-Closed Topology

Informal description

For any elements $a$, $b$, and $x$ in a topological space $\alpha$ with a preorder and an order-closed topology, if $a < x < b$, then the left-closed right-open interval $[a, b)$ is a neighborhood of $x$.

Icc_mem_nhds theorem

{a b x : α} (ha : a < x) (hb : x < b) : Icc a b ∈ 𝓝 x

Full source

theorem Icc_mem_nhds {a b x : α} (ha : a < x) (hb : x < b) : IccIcc a b ∈ 𝓝 x :=
  mem_of_superset (Ioo_mem_nhds ha hb) Ioo_subset_Icc_self

Closed Interval is a Neighborhood in Order-Closed Topology

Informal description

For any elements $a$, $b$, and $x$ in a topological space $\alpha$ with a preorder and an order-closed topology, if $a < x < b$, then the closed interval $[a, b]$ is a neighborhood of $x$.

DiscreteTopology.of_predOrder_succOrder theorem

[PredOrder α] [SuccOrder α] : DiscreteTopology α

Full source

/-- The only order closed topology on a linear order which is a `PredOrder` and a `SuccOrder`
is the discrete topology.

This theorem is not an instance,
because it causes searches for `PredOrder` and `SuccOrder` with their `Preorder` arguments
and very rarely matches. -/
theorem DiscreteTopology.of_predOrder_succOrder [PredOrder α] [SuccOrder α] :
    DiscreteTopology α := by
  refine discreteTopology_iff_nhds.mpr fun a ↦ ?_
  rw [← nhdsWithin_univ, ← Iic_union_Ioi, nhdsWithin_union, PredOrder.nhdsLE, SuccOrder.nhdsGT,
    sup_bot_eq]

Discrete Topology Characterization via PredOrder and SuccOrder

Informal description

Let $\alpha$ be a topological space equipped with a linear order. If $\alpha$ has both a predecessor order structure (`PredOrder`) and a successor order structure (`SuccOrder`), then the only order-closed topology on $\alpha$ is the discrete topology.

lt_subset_interior_le theorem

(hf : Continuous f) (hg : Continuous g) : {b | f b < g b} ⊆ interior {b | f b ≤ g b}

Full source

theorem lt_subset_interior_le (hf : Continuous f) (hg : Continuous g) :
    { b | f b < g b }{ b | f b < g b } ⊆ interior { b | f b ≤ g b } :=
  (interior_maximal fun _ => le_of_lt) <| isOpen_lt hf hg

Strict Sublevel Set is Contained in Interior of Non-Strict Sublevel Set

Informal description

Let $\alpha$ be a topological space with a preorder and an order-closed topology, and let $\beta$ be another topological space. For any continuous functions $f, g \colon \beta \to \alpha$, the set $\{b \in \beta \mid f(b) < g(b)\}$ is contained in the interior of the set $\{b \in \beta \mid f(b) \leq g(b)\}$.

frontier_le_subset_eq theorem

(hf : Continuous f) (hg : Continuous g) : frontier {b | f b ≤ g b} ⊆ {b | f b = g b}

Full source

theorem frontier_le_subset_eq (hf : Continuous f) (hg : Continuous g) :
    frontierfrontier { b | f b ≤ g b } ⊆ { b | f b = g b } := by
  rw [frontier_eq_closure_inter_closure, closure_le_eq hf hg]
  rintro b ⟨hb₁, hb₂⟩
  refine le_antisymm hb₁ (closure_lt_subset_le hg hf ?_)
  convert hb₂ using 2; simp only [not_le.symm]; rfl

Frontier of Sublevel Set is Contained in Level Set for Continuous Functions

Informal description

Let $\alpha$ be a topological space with a preorder and order-closed topology, and let $\beta$ be another topological space. For any continuous functions $f, g \colon \beta \to \alpha$, the frontier of the set $\{b \in \beta \mid f(b) \leq g(b)\}$ is contained in the set $\{b \in \beta \mid f(b) = g(b)\}$.

frontier_Iic_subset theorem

(a : α) : frontier (Iic a) ⊆ { a }

Full source

theorem frontier_Iic_subset (a : α) : frontierfrontier (Iic a) ⊆ {a} :=
  frontier_le_subset_eq (@continuous_id α _) continuous_const

Frontier of Left-Infinite Right-Closed Interval is Contained in Singleton

Informal description

For any element $a$ in a topological space $\alpha$ with a preorder and order-closed topology, the frontier of the left-infinite right-closed interval $(-\infty, a]$ is contained in the singleton set $\{a\}$.

frontier_Ici_subset theorem

(a : α) : frontier (Ici a) ⊆ { a }

Full source

theorem frontier_Ici_subset (a : α) : frontierfrontier (Ici a) ⊆ {a} :=
  frontier_Iic_subset (α := αᵒᵈ) _

Frontier of Right-Infinite Left-Closed Interval is Contained in Singleton

Informal description

For any element $a$ in a topological space $\alpha$ with a preorder and order-closed topology, the frontier of the right-infinite left-closed interval $[a, \infty)$ is contained in the singleton set $\{a\}$.

frontier_lt_subset_eq theorem

(hf : Continuous f) (hg : Continuous g) : frontier {b | f b < g b} ⊆ {b | f b = g b}

Full source

theorem frontier_lt_subset_eq (hf : Continuous f) (hg : Continuous g) :
    frontierfrontier { b | f b < g b } ⊆ { b | f b = g b } := by
  simpa only [← not_lt, ← compl_setOf, frontier_compl, eq_comm] using frontier_le_subset_eq hg hf

Frontier of Strict Sublevel Set is Contained in Level Set for Continuous Functions

Informal description

Let $\alpha$ be a topological space with a preorder and order-closed topology, and let $\beta$ be another topological space. For any continuous functions $f, g \colon \beta \to \alpha$, the frontier of the set $\{b \in \beta \mid f(b) < g(b)\}$ is contained in the set $\{b \in \beta \mid f(b) = g(b)\}$.

continuous_if_le theorem

 [TopologicalSpace γ] [∀ x, Decidable (f x ≤ g x)] {f' g' : β → γ} (hf : Continuous f) (hg : Continuous g)
  (hf' : ContinuousOn f' {x | f x ≤ g x}) (hg' : ContinuousOn g' {x | g x ≤ f x}) (hfg : ∀ x, f x = g x → f' x = g' x) :
  Continuous fun x => if f x ≤ g x then f' x else g' x

Full source

theorem continuous_if_le [TopologicalSpace γ] [∀ x, Decidable (f x ≤ g x)] {f' g' : β → γ}
    (hf : Continuous f) (hg : Continuous g) (hf' : ContinuousOn f' { x | f x ≤ g x })
    (hg' : ContinuousOn g' { x | g x ≤ f x }) (hfg : ∀ x, f x = g x → f' x = g' x) :
    Continuous fun x => if f x ≤ g x then f' x else g' x := by
  refine continuous_if (fun a ha => hfg _ (frontier_le_subset_eq hf hg ha)) ?_ (hg'.mono ?_)
  · rwa [(isClosed_le hf hg).closure_eq]
  · simp only [not_le]
    exact closure_lt_subset_le hg hf

Continuity of Conditional Function Based on Order Comparison

Informal description

Let $\alpha$ be a topological space with a preorder and order-closed topology, and let $\beta$ and $\gamma$ be topological spaces. Given continuous functions $f, g \colon \beta \to \alpha$ and functions $f', g' \colon \beta \to \gamma$ such that: 1. $f'$ is continuous on $\{x \in \beta \mid f(x) \leq g(x)\}$, 2. $g'$ is continuous on $\{x \in \beta \mid g(x) \leq f(x)\}$, 3. For all $x \in \beta$, if $f(x) = g(x)$, then $f'(x) = g'(x)$, then the function defined by \[ x \mapsto \begin{cases} f'(x) & \text{if } f(x) \leq g(x), \\ g'(x) & \text{otherwise}, \end{cases} \] is continuous on $\beta$.

Continuous.if_le theorem

 [TopologicalSpace γ] [∀ x, Decidable (f x ≤ g x)] {f' g' : β → γ} (hf' : Continuous f') (hg' : Continuous g')
  (hf : Continuous f) (hg : Continuous g) (hfg : ∀ x, f x = g x → f' x = g' x) :
  Continuous fun x => if f x ≤ g x then f' x else g' x

Full source

theorem Continuous.if_le [TopologicalSpace γ] [∀ x, Decidable (f x ≤ g x)] {f' g' : β → γ}
    (hf' : Continuous f') (hg' : Continuous g') (hf : Continuous f) (hg : Continuous g)
    (hfg : ∀ x, f x = g x → f' x = g' x) : Continuous fun x => if f x ≤ g x then f' x else g' x :=
  continuous_if_le hf hg hf'.continuousOn hg'.continuousOn hfg

Continuity of Conditional Function Based on Order Comparison with Continuous Components

Informal description

Let $\alpha$ be a topological space with a preorder and order-closed topology, and let $\beta$ and $\gamma$ be topological spaces. Given continuous functions $f, g \colon \beta \to \alpha$ and continuous functions $f', g' \colon \beta \to \gamma$ such that for all $x \in \beta$, if $f(x) = g(x)$, then $f'(x) = g'(x)$, the function defined by \[ x \mapsto \begin{cases} f'(x) & \text{if } f(x) \leq g(x), \\ g'(x) & \text{otherwise}, \end{cases} \] is continuous on $\beta$.

Filter.Tendsto.eventually_lt theorem

 {l : Filter γ} {f g : γ → α} {y z : α} (hf : Tendsto f l (𝓝 y)) (hg : Tendsto g l (𝓝 z)) (hyz : y < z) :
  ∀ᶠ x in l, f x < g x

Full source

theorem Filter.Tendsto.eventually_lt {l : Filter γ} {f g : γ → α} {y z : α} (hf : Tendsto f l (𝓝 y))
    (hg : Tendsto g l (𝓝 z)) (hyz : y < z) : ∀ᶠ x in l, f x < g x :=
  let ⟨_a, ha, _b, hb, h⟩ := hyz.exists_disjoint_Iio_Ioi
  (hg.eventually (Ioi_mem_nhds hb)).mp <| (hf.eventually (Iio_mem_nhds ha)).mono fun _ h₁ h₂ =>
    h _ h₁ _ h₂

Eventual Inequality Preservation under Filter Convergence

Informal description

Let $f, g : \gamma \to \alpha$ be functions and $l$ a filter on $\gamma$. If $f$ tends to $y$ along $l$, $g$ tends to $z$ along $l$, and $y < z$, then eventually for all $x$ in $l$, we have $f(x) < g(x)$.

ContinuousAt.eventually_lt theorem

 {x₀ : β} (hf : ContinuousAt f x₀) (hg : ContinuousAt g x₀) (hfg : f x₀ < g x₀) : ∀ᶠ x in 𝓝 x₀, f x < g x

Full source

nonrec theorem ContinuousAt.eventually_lt {x₀ : β} (hf : ContinuousAt f x₀) (hg : ContinuousAt g x₀)
    (hfg : f x₀ < g x₀) : ∀ᶠ x in 𝓝 x₀, f x < g x :=
  hf.eventually_lt hg hfg

Local Preservation of Strict Inequality under Continuous Functions

Informal description

Let $f, g : \beta \to \alpha$ be functions between topological spaces, and let $x_0 \in \beta$. If $f$ and $g$ are continuous at $x_0$ and $f(x_0) < g(x_0)$, then there exists a neighborhood of $x_0$ such that for all $x$ in this neighborhood, $f(x) < g(x)$.

Continuous.min theorem

(hf : Continuous f) (hg : Continuous g) : Continuous fun b => min (f b) (g b)

Full source

@[continuity, fun_prop]
protected theorem Continuous.min (hf : Continuous f) (hg : Continuous g) :
    Continuous fun b => min (f b) (g b) := by
  simp only [min_def]
  exact hf.if_le hg hf hg fun x => id

Continuity of Pointwise Minimum of Continuous Functions

Informal description

If $f, g \colon \beta \to \alpha$ are continuous functions between topological spaces, then the function $x \mapsto \min(f(x), g(x))$ is also continuous.

Continuous.max theorem

(hf : Continuous f) (hg : Continuous g) : Continuous fun b => max (f b) (g b)

Full source

@[continuity, fun_prop]
protected theorem Continuous.max (hf : Continuous f) (hg : Continuous g) :
    Continuous fun b => max (f b) (g b) :=
  Continuous.min (α := αᵒᵈ) hf hg

Continuity of Pointwise Maximum of Continuous Functions

Informal description

If $f, g \colon \beta \to \alpha$ are continuous functions between topological spaces, then the function $x \mapsto \max(f(x), g(x))$ is also continuous.

continuous_min theorem

: Continuous fun p : α × α => min p.1 p.2

Full source

theorem continuous_min : Continuous fun p : α × α => min p.1 p.2 :=
  continuous_fst.min continuous_snd

Continuity of the Minimum Function

Informal description

The function $\min \colon \alpha \times \alpha \to \alpha$ is continuous with respect to the product topology on $\alpha \times \alpha$ and the given topology on $\alpha$.

continuous_max theorem

: Continuous fun p : α × α => max p.1 p.2

Full source

theorem continuous_max : Continuous fun p : α × α => max p.1 p.2 :=
  continuous_fst.max continuous_snd

Continuity of the Maximum Function

Informal description

The function $\max \colon \alpha \times \alpha \to \alpha$ is continuous with respect to the product topology on $\alpha \times \alpha$ and the given topology on $\alpha$.

Filter.Tendsto.max theorem

 {b : Filter β} {a₁ a₂ : α} (hf : Tendsto f b (𝓝 a₁)) (hg : Tendsto g b (𝓝 a₂)) :
  Tendsto (fun b => max (f b) (g b)) b (𝓝 (max a₁ a₂))

Full source

protected theorem Filter.Tendsto.max {b : Filter β} {a₁ a₂ : α} (hf : Tendsto f b (𝓝 a₁))
    (hg : Tendsto g b (𝓝 a₂)) : Tendsto (fun b => max (f b) (g b)) b (𝓝 (max a₁ a₂)) :=
  (continuous_max.tendsto (a₁, a₂)).comp (hf.prodMk_nhds hg)

Limit of Pointwise Maximum is Maximum of Limits

Informal description

Let $f, g \colon \beta \to \alpha$ be functions such that $f$ tends to $a_1$ and $g$ tends to $a_2$ along a filter $b$. Then the pointwise maximum function $x \mapsto \max(f(x), g(x))$ tends to $\max(a_1, a_2)$ along the same filter $b$.

Filter.Tendsto.min theorem

 {b : Filter β} {a₁ a₂ : α} (hf : Tendsto f b (𝓝 a₁)) (hg : Tendsto g b (𝓝 a₂)) :
  Tendsto (fun b => min (f b) (g b)) b (𝓝 (min a₁ a₂))

Full source

protected theorem Filter.Tendsto.min {b : Filter β} {a₁ a₂ : α} (hf : Tendsto f b (𝓝 a₁))
    (hg : Tendsto g b (𝓝 a₂)) : Tendsto (fun b => min (f b) (g b)) b (𝓝 (min a₁ a₂)) :=
  (continuous_min.tendsto (a₁, a₂)).comp (hf.prodMk_nhds hg)

Limit of Pointwise Minimum is Minimum of Limits

Informal description

Let $f, g \colon \beta \to \alpha$ be functions such that $f$ tends to $a_1$ and $g$ tends to $a_2$ along a filter $b$. Then the pointwise minimum function $x \mapsto \min(f(x), g(x))$ tends to $\min(a_1, a_2)$ along the same filter $b$.

Filter.Tendsto.max_right theorem

{l : Filter β} {a : α} (h : Tendsto f l (𝓝 a)) : Tendsto (fun i => max a (f i)) l (𝓝 a)

Full source

protected theorem Filter.Tendsto.max_right {l : Filter β} {a : α} (h : Tendsto f l (𝓝 a)) :
    Tendsto (fun i => max a (f i)) l (𝓝 a) := by
  simpa only [sup_idem] using (tendsto_const_nhds (x := a)).max h

Limit of Maximum with Constant is Constant

Informal description

Let $f \colon \beta \to \alpha$ be a function that tends to $a$ along a filter $l$. Then the function $x \mapsto \max(a, f(x))$ tends to $a$ along the same filter $l$.

Filter.Tendsto.max_left theorem

{l : Filter β} {a : α} (h : Tendsto f l (𝓝 a)) : Tendsto (fun i => max (f i) a) l (𝓝 a)

Full source

protected theorem Filter.Tendsto.max_left {l : Filter β} {a : α} (h : Tendsto f l (𝓝 a)) :
    Tendsto (fun i => max (f i) a) l (𝓝 a) := by
  simp_rw [max_comm _ a]
  exact h.max_right

Limit of Maximum with Constant is Constant (Left Variant)

Informal description

Let $f \colon \beta \to \alpha$ be a function that tends to $a$ along a filter $l$. Then the function $x \mapsto \max(f(x), a)$ tends to $a$ along the same filter $l$.

Filter.tendsto_nhds_max_right theorem

{l : Filter β} {a : α} (h : Tendsto f l (𝓝[>] a)) : Tendsto (fun i => max a (f i)) l (𝓝[>] a)

Full source

theorem Filter.tendsto_nhds_max_right {l : Filter β} {a : α} (h : Tendsto f l (𝓝[>] a)) :
    Tendsto (fun i => max a (f i)) l (𝓝[>] a) := by
  obtain ⟨h₁ : Tendsto f l (𝓝 a), h₂ : ∀ᶠ i in l, f i ∈ Ioi a⟩ := tendsto_nhdsWithin_iff.mp h
  exact tendsto_nhdsWithin_iff.mpr ⟨h₁.max_right, h₂.mono fun i hi => lt_max_of_lt_right hi⟩

Limit of Maximum with Constant Preserves Right-Neighborhood Convergence

Informal description

Let $α$ be a topological space with a preorder and order-closed topology, and let $β$ be another type. For any function $f \colon β \to α$ and any filter $l$ on $β$, if $f$ tends to $a$ along the right-neighborhood filter $\mathcal{N}_{>a}$ (i.e., the filter of neighborhoods to the right of $a$), then the function $x \mapsto \max(a, f(x))$ also tends to $a$ along $\mathcal{N}_{>a}$.

Filter.tendsto_nhds_max_left theorem

{l : Filter β} {a : α} (h : Tendsto f l (𝓝[>] a)) : Tendsto (fun i => max (f i) a) l (𝓝[>] a)

Full source

theorem Filter.tendsto_nhds_max_left {l : Filter β} {a : α} (h : Tendsto f l (𝓝[>] a)) :
    Tendsto (fun i => max (f i) a) l (𝓝[>] a) := by
  simp_rw [max_comm _ a]
  exact Filter.tendsto_nhds_max_right h

Limit of Maximum with Constant Preserves Right-Neighborhood Convergence (Left Variant)

Informal description

Let $α$ be a topological space with a preorder and order-closed topology, and let $β$ be another type. For any function $f \colon β \to α$ and any filter $l$ on $β$, if $f$ tends to $a$ along the right-neighborhood filter $\mathcal{N}_{>a}$ (i.e., the filter of neighborhoods to the right of $a$), then the function $x \mapsto \max(f(x), a)$ also tends to $a$ along $\mathcal{N}_{>a}$.

Filter.Tendsto.min_right theorem

{l : Filter β} {a : α} (h : Tendsto f l (𝓝 a)) : Tendsto (fun i => min a (f i)) l (𝓝 a)

Full source

theorem Filter.Tendsto.min_right {l : Filter β} {a : α} (h : Tendsto f l (𝓝 a)) :
    Tendsto (fun i => min a (f i)) l (𝓝 a) :=
  Filter.Tendsto.max_right (α := αᵒᵈ) h

Limit of Minimum with Constant is Constant

Informal description

Let $f \colon \beta \to \alpha$ be a function that tends to $a$ along a filter $l$. Then the function $x \mapsto \min(a, f(x))$ tends to $a$ along the same filter $l$.

Filter.tendsto_nhds_min_right theorem

{l : Filter β} {a : α} (h : Tendsto f l (𝓝[<] a)) : Tendsto (fun i => min a (f i)) l (𝓝[<] a)

Full source

theorem Filter.tendsto_nhds_min_right {l : Filter β} {a : α} (h : Tendsto f l (𝓝[<] a)) :
    Tendsto (fun i => min a (f i)) l (𝓝[<] a) :=
  Filter.tendsto_nhds_max_right (α := αᵒᵈ) h

Limit of Minimum with Constant Preserves Left-Neighborhood Convergence

Informal description

Let $\alpha$ be a topological space with a preorder and order-closed topology, and let $\beta$ be another type. For any function $f \colon \beta \to \alpha$ and any filter $l$ on $\beta$, if $f$ tends to $a$ along the left-neighborhood filter $\mathcal{N}_{

Dense.exists_between theorem

[DenselyOrdered α] {s : Set α} (hs : Dense s) {x y : α} (h : x < y) : ∃ z ∈ s, z ∈ Ioo x y

Full source

theorem Dense.exists_between [DenselyOrdered α] {s : Set α} (hs : Dense s) {x y : α} (h : x < y) :
    ∃ z ∈ s, z ∈ Ioo x y :=
  hs.exists_mem_open isOpen_Ioo (nonempty_Ioo.2 h)

Existence of Dense Elements in Open Intervals

Informal description

Let $\alpha$ be a densely ordered set, and let $s$ be a dense subset of $\alpha$. For any two elements $x, y \in \alpha$ with $x < y$, there exists an element $z \in s$ such that $z$ lies strictly between $x$ and $y$, i.e., $x < z < y$.

Dense.Ioi_eq_biUnion theorem

[DenselyOrdered α] {s : Set α} (hs : Dense s) (x : α) : Ioi x = ⋃ y ∈ s ∩ Ioi x, Ioi y

Full source

theorem Dense.Ioi_eq_biUnion [DenselyOrdered α] {s : Set α} (hs : Dense s) (x : α) :
    Ioi x = ⋃ y ∈ s ∩ Ioi x, Ioi y := by
  refine Subset.antisymm (fun z hz ↦ ?_) (iUnion₂_subset fun y hy ↦ Ioi_subset_Ioi (le_of_lt hy.2))
  rcases hs.exists_between hz with ⟨y, hys, hxy, hyz⟩
  exact mem_iUnion₂.2 ⟨y, ⟨hys, hxy⟩, hyz⟩

Decomposition of Right-Infinite Open Interval via Dense Subset

Informal description

Let $\alpha$ be a densely ordered set, and let $s$ be a dense subset of $\alpha$. For any element $x \in \alpha$, the right-infinite open interval $(x, \infty)$ can be expressed as the union of all right-infinite open intervals $(y, \infty)$ where $y$ ranges over elements of $s$ that are greater than $x$. In other words: $$ (x, \infty) = \bigcup_{y \in s \cap (x, \infty)} (y, \infty). $$

Dense.Iio_eq_biUnion theorem

[DenselyOrdered α] {s : Set α} (hs : Dense s) (x : α) : Iio x = ⋃ y ∈ s ∩ Iio x, Iio y

Full source

theorem Dense.Iio_eq_biUnion [DenselyOrdered α] {s : Set α} (hs : Dense s) (x : α) :
    Iio x = ⋃ y ∈ s ∩ Iio x, Iio y :=
  Dense.Ioi_eq_biUnion (α := αᵒᵈ) hs x

Decomposition of Left-Infinite Open Interval via Dense Subset

Informal description

Let $\alpha$ be a densely ordered set, and let $s$ be a dense subset of $\alpha$. For any element $x \in \alpha$, the left-infinite open interval $(-\infty, x)$ can be expressed as the union of all left-infinite open intervals $(-\infty, y)$ where $y$ ranges over elements of $s$ that are less than $x$. In other words: $$ (-\infty, x) = \bigcup_{y \in s \cap (-\infty, x)} (-\infty, y). $$

instOrderClosedTopologyProd instance

 [Preorder α] [TopologicalSpace α] [OrderClosedTopology α] [Preorder β] [TopologicalSpace β] [OrderClosedTopology β] :
  OrderClosedTopology (α × β)

Full source

instance [Preorder α] [TopologicalSpace α] [OrderClosedTopology α] [Preorder β] [TopologicalSpace β]
    [OrderClosedTopology β] : OrderClosedTopology (α × β) :=
  ⟨(isClosed_le continuous_fst.fst continuous_snd.fst).inter
    (isClosed_le continuous_fst.snd continuous_snd.snd)⟩

Product of Order-Closed Topological Spaces is Order-Closed

Informal description

For any two preordered topological spaces $\alpha$ and $\beta$ with order-closed topologies, the product space $\alpha \times \beta$ also has an order-closed topology. This means that the set $\{(x, y) \in \alpha \times \beta \mid x \leq y\}$ is closed in the product topology.

instOrderClosedTopologyForall instance

 {ι : Type*} {α : ι → Type*} [∀ i, Preorder (α i)] [∀ i, TopologicalSpace (α i)] [∀ i, OrderClosedTopology (α i)] :
  OrderClosedTopology (∀ i, α i)

Full source

instance {ι : Type*} {α : ι → Type*} [∀ i, Preorder (α i)] [∀ i, TopologicalSpace (α i)]
    [∀ i, OrderClosedTopology (α i)] : OrderClosedTopology (∀ i, α i) := by
  constructor
  simp only [Pi.le_def, setOf_forall]
  exact isClosed_iInter fun i => isClosed_le (continuous_apply i).fst' (continuous_apply i).snd'

Product of Order-Closed Topological Spaces is Order-Closed

Informal description

For any family of preordered topological spaces $\{\alpha_i\}_{i \in \iota}$ where each $\alpha_i$ has an order-closed topology, the product space $\prod_{i \in \iota} \alpha_i$ also has an order-closed topology. This means that the set $\{(x_i)_{i \in \iota} \mid \forall i, x_i \leq y_i\}$ is closed in the product topology for any $(y_i)_{i \in \iota} \in \prod_{i \in \iota} \alpha_i$.

Pi.orderClosedTopology' instance

[Preorder β] [TopologicalSpace β] [OrderClosedTopology β] : OrderClosedTopology (α → β)

Full source

instance Pi.orderClosedTopology' [Preorder β] [TopologicalSpace β] [OrderClosedTopology β] :
    OrderClosedTopology (α → β) :=
  inferInstance

Function Space with Order-Closed Topology

Informal description

For any preordered topological space $\beta$ with an order-closed topology, the function space $\alpha \to \beta$ also has an order-closed topology. This means that the set $\{f \colon \alpha \to \beta \mid \forall x, f(x) \leq g(x)\}$ is closed in the product topology for any $g \colon \alpha \to \beta$.

Mathlib.Topology.Order.OrderClosed

Main statements

Open / closed sets

Convergence and inequalities

Min, max, `sSup` and `sInf`

Main statements

Open / closed sets

Convergence and inequalities

Min, max, sSup and sInf

Min, max, `sSup` and `sInf`