Mathlib.Topology.Order.MonotoneContinuity

StrictMonoOn.continuousWithinAt_right_of_exists_between theorem

 {f : α → β} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s ∈ 𝓝[≥] a)
  (hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b) : ContinuousWithinAt f (Ici a) a

Full source

/-- If `f` is a function strictly monotone on a right neighborhood of `a` and the
image of this neighborhood under `f` meets every interval `(f a, b]`, `b > f a`, then `f` is
continuous at `a` from the right.

The assumption `hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b` is required because otherwise the
function `f : ℝ → ℝ` given by `f x = if x ≤ 0 then x else x + 1` would be a counter-example at
`a = 0`. -/
theorem StrictMonoOn.continuousWithinAt_right_of_exists_between {f : α → β} {s : Set α} {a : α}
    (h_mono : StrictMonoOn f s) (hs : s ∈ 𝓝[≥] a) (hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b) :
    ContinuousWithinAt f (Ici a) a := by
  have ha : a ∈ Ici a := left_mem_Ici
  have has : a ∈ s := mem_of_mem_nhdsWithin ha hs
  refine tendsto_order.2 ⟨fun b hb => ?_, fun b hb => ?_⟩
  · filter_upwards [hs, @self_mem_nhdsWithin _ _ a (Ici a)] with _ hxs hxa using hb.trans_le
      ((h_mono.le_iff_le has hxs).2 hxa)
  · rcases hfs b hb with ⟨c, hcs, hac, hcb⟩
    rw [h_mono.lt_iff_lt has hcs] at hac
    filter_upwards [hs, Ico_mem_nhdsGE hac]
    rintro x hx ⟨_, hxc⟩
    exact ((h_mono.lt_iff_lt hx hcs).2 hxc).trans_le hcb

Right Continuity of Strictly Increasing Functions with Intermediate Value Property

Informal description

Let $f : \alpha \to \beta$ be a function strictly increasing on a set $s \subseteq \alpha$ that is a right-neighborhood of $a \in \alpha$. Suppose that for every $b > f(a)$, there exists $c \in s$ such that $f(c) \in (f(a), b]$. Then $f$ is continuous at $a$ from the right, i.e., continuous within the interval $[a, \infty)$ at $a$.

continuousWithinAt_right_of_monotoneOn_of_exists_between theorem

 {f : α → β} {s : Set α} {a : α} (h_mono : MonotoneOn f s) (hs : s ∈ 𝓝[≥] a)
  (hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b) : ContinuousWithinAt f (Ici a) a

Full source

/-- If `f` is a monotone function on a right neighborhood of `a` and the image of this neighborhood
under `f` meets every interval `(f a, b)`, `b > f a`, then `f` is continuous at `a` from the right.

The assumption `hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b` cannot be replaced by the weaker
assumption `hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b` we use for strictly monotone functions
because otherwise the function `ceil : ℝ → ℤ` would be a counter-example at `a = 0`. -/
theorem continuousWithinAt_right_of_monotoneOn_of_exists_between {f : α → β} {s : Set α} {a : α}
    (h_mono : MonotoneOn f s) (hs : s ∈ 𝓝[≥] a) (hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b) :
    ContinuousWithinAt f (Ici a) a := by
  have ha : a ∈ Ici a := left_mem_Ici
  have has : a ∈ s := mem_of_mem_nhdsWithin ha hs
  refine tendsto_order.2 ⟨fun b hb => ?_, fun b hb => ?_⟩
  · filter_upwards [hs, @self_mem_nhdsWithin _ _ a (Ici a)] with _ hxs hxa using hb.trans_le
      (h_mono has hxs hxa)
  · rcases hfs b hb with ⟨c, hcs, hac, hcb⟩
    have : a < c := not_le.1 fun h => hac.not_le <| h_mono hcs has h
    filter_upwards [hs, Ico_mem_nhdsGE this]
    rintro x hx ⟨_, hxc⟩
    exact (h_mono hx hcs hxc.le).trans_lt hcb

Right Continuity of Monotone Functions with Intermediate Value Property

Informal description

Let $f : \alpha \to \beta$ be a function that is monotone on a set $s \subseteq \alpha$ which is a right-neighborhood of $a \in \alpha$. Suppose that for every $b > f(a)$, there exists $c \in s$ such that $f(c) \in (f(a), b)$. Then $f$ is continuous at $a$ from the right, i.e., continuous within the interval $[a, \infty)$ at $a$.

continuousWithinAt_right_of_monotoneOn_of_closure_image_mem_nhdsWithin theorem

 [DenselyOrdered β] {f : α → β} {s : Set α} {a : α} (h_mono : MonotoneOn f s) (hs : s ∈ 𝓝[≥] a)
  (hfs : closure (f '' s) ∈ 𝓝[≥] f a) : ContinuousWithinAt f (Ici a) a

Full source

/-- If a function `f` with a densely ordered codomain is monotone on a right neighborhood of `a` and
the closure of the image of this neighborhood under `f` is a right neighborhood of `f a`, then `f`
is continuous at `a` from the right. -/
theorem continuousWithinAt_right_of_monotoneOn_of_closure_image_mem_nhdsWithin [DenselyOrdered β]
    {f : α → β} {s : Set α} {a : α} (h_mono : MonotoneOn f s) (hs : s ∈ 𝓝[≥] a)
    (hfs : closureclosure (f '' s) ∈ 𝓝[≥] f a) : ContinuousWithinAt f (Ici a) a := by
  refine continuousWithinAt_right_of_monotoneOn_of_exists_between h_mono hs fun b hb => ?_
  rcases (mem_nhdsGE_iff_exists_mem_Ioc_Ico_subset hb).1 hfs with ⟨b', ⟨hab', hbb'⟩, hb'⟩
  rcases exists_between hab' with ⟨c', hc'⟩
  rcases mem_closure_iff.1 (hb' ⟨hc'.1.le, hc'.2⟩) (Ioo (f a) b') isOpen_Ioo hc' with
    ⟨_, hc, ⟨c, hcs, rfl⟩⟩
  exact ⟨c, hcs, hc.1, hc.2.trans_le hbb'⟩

Right Continuity of Monotone Functions via Closure Condition

Informal description

Let $\alpha$ and $\beta$ be topological spaces with $\beta$ densely ordered. Let $f : \alpha \to \beta$ be a function that is monotone on a set $s \subseteq \alpha$ which is a right-neighborhood of $a \in \alpha$. If the closure of the image $f(s)$ is a right-neighborhood of $f(a)$, then $f$ is continuous at $a$ from the right, i.e., continuous within the interval $[a, \infty)$ at $a$.

continuousWithinAt_right_of_monotoneOn_of_image_mem_nhdsWithin theorem

 [DenselyOrdered β] {f : α → β} {s : Set α} {a : α} (h_mono : MonotoneOn f s) (hs : s ∈ 𝓝[≥] a)
  (hfs : f '' s ∈ 𝓝[≥] f a) : ContinuousWithinAt f (Ici a) a

Full source

/-- If a function `f` with a densely ordered codomain is monotone on a right neighborhood of `a` and
the image of this neighborhood under `f` is a right neighborhood of `f a`, then `f` is continuous at
`a` from the right. -/
theorem continuousWithinAt_right_of_monotoneOn_of_image_mem_nhdsWithin [DenselyOrdered β]
    {f : α → β} {s : Set α} {a : α} (h_mono : MonotoneOn f s) (hs : s ∈ 𝓝[≥] a)
    (hfs : f '' sf '' s ∈ 𝓝[≥] f a) : ContinuousWithinAt f (Ici a) a :=
  continuousWithinAt_right_of_monotoneOn_of_closure_image_mem_nhdsWithin h_mono hs <|
    mem_of_superset hfs subset_closure

Right Continuity of Monotone Functions via Image Neighborhood Condition

Informal description

Let $\alpha$ and $\beta$ be topological spaces with $\beta$ densely ordered. Let $f : \alpha \to \beta$ be a function that is monotone on a set $s \subseteq \alpha$ which is a right-neighborhood of $a \in \alpha$. If the image $f(s)$ is a right-neighborhood of $f(a)$, then $f$ is continuous at $a$ from the right, i.e., continuous within the interval $[a, \infty)$ at $a$.

StrictMonoOn.continuousWithinAt_right_of_closure_image_mem_nhdsWithin theorem

 [DenselyOrdered β] {f : α → β} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s ∈ 𝓝[≥] a)
  (hfs : closure (f '' s) ∈ 𝓝[≥] f a) : ContinuousWithinAt f (Ici a) a

Full source

/-- If a function `f` with a densely ordered codomain is strictly monotone on a right neighborhood
of `a` and the closure of the image of this neighborhood under `f` is a right neighborhood of `f a`,
then `f` is continuous at `a` from the right. -/
theorem StrictMonoOn.continuousWithinAt_right_of_closure_image_mem_nhdsWithin [DenselyOrdered β]
    {f : α → β} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s ∈ 𝓝[≥] a)
    (hfs : closureclosure (f '' s) ∈ 𝓝[≥] f a) : ContinuousWithinAt f (Ici a) a :=
  continuousWithinAt_right_of_monotoneOn_of_closure_image_mem_nhdsWithin
    (fun _ hx _ hy => (h_mono.le_iff_le hx hy).2) hs hfs

Right Continuity of Strictly Increasing Functions via Closure Condition

Informal description

Let $\alpha$ and $\beta$ be topological spaces with $\beta$ densely ordered. Let $f : \alpha \to \beta$ be a function that is strictly increasing on a set $s \subseteq \alpha$ which is a right-neighborhood of $a \in \alpha$. If the closure of the image $f(s)$ is a right-neighborhood of $f(a)$, then $f$ is continuous at $a$ from the right, i.e., continuous within the interval $[a, \infty)$ at $a$.

StrictMonoOn.continuousWithinAt_right_of_image_mem_nhdsWithin theorem

 [DenselyOrdered β] {f : α → β} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s ∈ 𝓝[≥] a)
  (hfs : f '' s ∈ 𝓝[≥] f a) : ContinuousWithinAt f (Ici a) a

Full source

/-- If a function `f` with a densely ordered codomain is strictly monotone on a right neighborhood
of `a` and the image of this neighborhood under `f` is a right neighborhood of `f a`, then `f` is
continuous at `a` from the right. -/
theorem StrictMonoOn.continuousWithinAt_right_of_image_mem_nhdsWithin [DenselyOrdered β] {f : α → β}
    {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s ∈ 𝓝[≥] a) (hfs : f '' sf '' s ∈ 𝓝[≥] f a) :
    ContinuousWithinAt f (Ici a) a :=
  h_mono.continuousWithinAt_right_of_closure_image_mem_nhdsWithin hs
    (mem_of_superset hfs subset_closure)

Right continuity of strictly increasing functions via image neighborhood condition

Informal description

Let $\alpha$ and $\beta$ be topological spaces with $\beta$ densely ordered. Let $f : \alpha \to \beta$ be a function that is strictly increasing on a set $s \subseteq \alpha$ which is a right-neighborhood of $a \in \alpha$. If the image $f(s)$ is a right-neighborhood of $f(a)$, then $f$ is continuous at $a$ from the right, i.e., continuous within the interval $[a, \infty)$ at $a$.

StrictMonoOn.continuousWithinAt_right_of_surjOn theorem

 {f : α → β} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s ∈ 𝓝[≥] a) (hfs : SurjOn f s (Ioi (f a))) :
  ContinuousWithinAt f (Ici a) a

Full source

/-- If a function `f` is strictly monotone on a right neighborhood of `a` and the image of this
neighborhood under `f` includes `Ioi (f a)`, then `f` is continuous at `a` from the right. -/
theorem StrictMonoOn.continuousWithinAt_right_of_surjOn {f : α → β} {s : Set α} {a : α}
    (h_mono : StrictMonoOn f s) (hs : s ∈ 𝓝[≥] a) (hfs : SurjOn f s (Ioi (f a))) :
    ContinuousWithinAt f (Ici a) a :=
  h_mono.continuousWithinAt_right_of_exists_between hs fun _ hb =>
    let ⟨c, hcs, hcb⟩ := hfs hb
    ⟨c, hcs, hcb.symm ▸ hb, hcb.le⟩

Right Continuity of Strictly Increasing Surjective Functions on Right-Neighborhoods

Informal description

Let $f : \alpha \to \beta$ be a function strictly increasing on a set $s \subseteq \alpha$ that is a right-neighborhood of $a \in \alpha$. If $f$ maps $s$ surjectively onto the right-infinite open interval $(f(a), \infty)$, then $f$ is continuous at $a$ from the right, i.e., continuous within the interval $[a, \infty)$ at $a$.

StrictMonoOn.continuousWithinAt_left_of_exists_between theorem

 {f : α → β} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s ∈ 𝓝[≤] a)
  (hfs : ∀ b < f a, ∃ c ∈ s, f c ∈ Ico b (f a)) : ContinuousWithinAt f (Iic a) a

Full source

/-- If `f` is a strictly monotone function on a left neighborhood of `a` and the image of this
neighborhood under `f` meets every interval `[b, f a)`, `b < f a`, then `f` is continuous at `a`
from the left.

The assumption `hfs : ∀ b < f a, ∃ c ∈ s, f c ∈ Ico b (f a)` is required because otherwise the
function `f : ℝ → ℝ` given by `f x = if x < 0 then x else x + 1` would be a counter-example at
`a = 0`. -/
theorem StrictMonoOn.continuousWithinAt_left_of_exists_between {f : α → β} {s : Set α} {a : α}
    (h_mono : StrictMonoOn f s) (hs : s ∈ 𝓝[≤] a) (hfs : ∀ b < f a, ∃ c ∈ s, f c ∈ Ico b (f a)) :
    ContinuousWithinAt f (Iic a) a :=
  h_mono.dual.continuousWithinAt_right_of_exists_between hs fun b hb =>
    let ⟨c, hcs, hcb, hca⟩ := hfs b hb
    ⟨c, hcs, hca, hcb⟩

Left Continuity of Strictly Increasing Functions with Intermediate Value Property

Informal description

Let $f : \alpha \to \beta$ be a function strictly increasing on a set $s \subseteq \alpha$ that is a left-neighborhood of $a \in \alpha$. Suppose that for every $b < f(a)$, there exists $c \in s$ such that $f(c) \in [b, f(a))$. Then $f$ is continuous at $a$ from the left, i.e., continuous within the interval $(-\infty, a]$ at $a$.

continuousWithinAt_left_of_monotoneOn_of_exists_between theorem

 {f : α → β} {s : Set α} {a : α} (hf : MonotoneOn f s) (hs : s ∈ 𝓝[≤] a) (hfs : ∀ b < f a, ∃ c ∈ s, f c ∈ Ioo b (f a)) :
  ContinuousWithinAt f (Iic a) a

Full source

/-- If `f` is a monotone function on a left neighborhood of `a` and the image of this neighborhood
under `f` meets every interval `(b, f a)`, `b < f a`, then `f` is continuous at `a` from the left.

The assumption `hfs : ∀ b < f a, ∃ c ∈ s, f c ∈ Ioo b (f a)` cannot be replaced by the weaker
assumption `hfs : ∀ b < f a, ∃ c ∈ s, f c ∈ Ico b (f a)` we use for strictly monotone functions
because otherwise the function `floor : ℝ → ℤ` would be a counter-example at `a = 0`. -/
theorem continuousWithinAt_left_of_monotoneOn_of_exists_between {f : α → β} {s : Set α} {a : α}
    (hf : MonotoneOn f s) (hs : s ∈ 𝓝[≤] a) (hfs : ∀ b < f a, ∃ c ∈ s, f c ∈ Ioo b (f a)) :
    ContinuousWithinAt f (Iic a) a :=
  @continuousWithinAt_right_of_monotoneOn_of_exists_between αᵒᵈ βᵒᵈ _ _ _ _ _ _ f s a hf.dual hs
    fun b hb =>
    let ⟨c, hcs, hcb, hca⟩ := hfs b hb
    ⟨c, hcs, hca, hcb⟩

Left Continuity of Monotone Functions with Intermediate Value Property

Informal description

Let $f : \alpha \to \beta$ be a function that is monotone on a set $s \subseteq \alpha$ which is a left-neighborhood of $a \in \alpha$. Suppose that for every $b < f(a)$, there exists $c \in s$ such that $f(c) \in (b, f(a))$. Then $f$ is continuous at $a$ from the left, i.e., continuous within the interval $(-\infty, a]$ at $a$.

continuousWithinAt_left_of_monotoneOn_of_closure_image_mem_nhdsWithin theorem

 [DenselyOrdered β] {f : α → β} {s : Set α} {a : α} (hf : MonotoneOn f s) (hs : s ∈ 𝓝[≤] a)
  (hfs : closure (f '' s) ∈ 𝓝[≤] f a) : ContinuousWithinAt f (Iic a) a

Full source

/-- If a function `f` with a densely ordered codomain is monotone on a left neighborhood of `a` and
the closure of the image of this neighborhood under `f` is a left neighborhood of `f a`, then `f` is
continuous at `a` from the left -/
theorem continuousWithinAt_left_of_monotoneOn_of_closure_image_mem_nhdsWithin [DenselyOrdered β]
    {f : α → β} {s : Set α} {a : α} (hf : MonotoneOn f s) (hs : s ∈ 𝓝[≤] a)
    (hfs : closureclosure (f '' s) ∈ 𝓝[≤] f a) : ContinuousWithinAt f (Iic a) a :=
  @continuousWithinAt_right_of_monotoneOn_of_closure_image_mem_nhdsWithin αᵒᵈ βᵒᵈ _ _ _ _ _ _ _ f s
    a hf.dual hs hfs

Left Continuity of Monotone Functions via Closure Condition

Informal description

Let $\alpha$ and $\beta$ be topological spaces with $\beta$ densely ordered. Let $f : \alpha \to \beta$ be a function that is monotone on a set $s \subseteq \alpha$ which is a left-neighborhood of $a \in \alpha$. If the closure of the image $f(s)$ is a left-neighborhood of $f(a)$, then $f$ is continuous at $a$ from the left, i.e., continuous within the interval $(-\infty, a]$ at $a$.

continuousWithinAt_left_of_monotoneOn_of_image_mem_nhdsWithin theorem

 [DenselyOrdered β] {f : α → β} {s : Set α} {a : α} (h_mono : MonotoneOn f s) (hs : s ∈ 𝓝[≤] a)
  (hfs : f '' s ∈ 𝓝[≤] f a) : ContinuousWithinAt f (Iic a) a

Full source

/-- If a function `f` with a densely ordered codomain is monotone on a left neighborhood of `a` and
the image of this neighborhood under `f` is a left neighborhood of `f a`, then `f` is continuous at
`a` from the left. -/
theorem continuousWithinAt_left_of_monotoneOn_of_image_mem_nhdsWithin [DenselyOrdered β] {f : α → β}
    {s : Set α} {a : α} (h_mono : MonotoneOn f s) (hs : s ∈ 𝓝[≤] a) (hfs : f '' sf '' s ∈ 𝓝[≤] f a) :
    ContinuousWithinAt f (Iic a) a :=
  continuousWithinAt_left_of_monotoneOn_of_closure_image_mem_nhdsWithin h_mono hs
    (mem_of_superset hfs subset_closure)

Left continuity of monotone functions with neighborhood condition

Informal description

Let $\alpha$ and $\beta$ be topological spaces with $\beta$ densely ordered. Let $f : \alpha \to \beta$ be a function that is monotone on a set $s \subseteq \alpha$ which is a left-neighborhood of $a \in \alpha$. If the image $f(s)$ is a left-neighborhood of $f(a)$, then $f$ is continuous at $a$ from the left, i.e., continuous within the interval $(-\infty, a]$.

StrictMonoOn.continuousWithinAt_left_of_closure_image_mem_nhdsWithin theorem

 [DenselyOrdered β] {f : α → β} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s ∈ 𝓝[≤] a)
  (hfs : closure (f '' s) ∈ 𝓝[≤] f a) : ContinuousWithinAt f (Iic a) a

Full source

/-- If a function `f` with a densely ordered codomain is strictly monotone on a left neighborhood of
`a` and the closure of the image of this neighborhood under `f` is a left neighborhood of `f a`,
then `f` is continuous at `a` from the left. -/
theorem StrictMonoOn.continuousWithinAt_left_of_closure_image_mem_nhdsWithin [DenselyOrdered β]
    {f : α → β} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s ∈ 𝓝[≤] a)
    (hfs : closureclosure (f '' s) ∈ 𝓝[≤] f a) : ContinuousWithinAt f (Iic a) a :=
  h_mono.dual.continuousWithinAt_right_of_closure_image_mem_nhdsWithin hs hfs

Left continuity of strictly increasing functions via closure condition

Informal description

Let $\alpha$ and $\beta$ be topological spaces with $\beta$ densely ordered. Let $f \colon \alpha \to \beta$ be a function that is strictly increasing on a set $s \subseteq \alpha$ which is a left-neighborhood of $a \in \alpha$. If the closure of the image $f(s)$ is a left-neighborhood of $f(a)$, then $f$ is continuous at $a$ from the left, i.e., continuous within the interval $(-\infty, a]$ at $a$.

StrictMonoOn.continuousWithinAt_left_of_image_mem_nhdsWithin theorem

 [DenselyOrdered β] {f : α → β} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s ∈ 𝓝[≤] a)
  (hfs : f '' s ∈ 𝓝[≤] f a) : ContinuousWithinAt f (Iic a) a

Full source

/-- If a function `f` with a densely ordered codomain is strictly monotone on a left neighborhood of
`a` and the image of this neighborhood under `f` is a left neighborhood of `f a`, then `f` is
continuous at `a` from the left. -/
theorem StrictMonoOn.continuousWithinAt_left_of_image_mem_nhdsWithin [DenselyOrdered β] {f : α → β}
    {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s ∈ 𝓝[≤] a) (hfs : f '' sf '' s ∈ 𝓝[≤] f a) :
    ContinuousWithinAt f (Iic a) a :=
  h_mono.dual.continuousWithinAt_right_of_image_mem_nhdsWithin hs hfs

Left continuity of strictly increasing functions via image neighborhood condition

Informal description

Let $\alpha$ and $\beta$ be topological spaces with $\beta$ densely ordered. Let $f : \alpha \to \beta$ be a function that is strictly increasing on a set $s \subseteq \alpha$ which is a left-neighborhood of $a \in \alpha$. If the image $f(s)$ is a left-neighborhood of $f(a)$, then $f$ is continuous at $a$ from the left, i.e., continuous within the interval $(-\infty, a]$.

StrictMonoOn.continuousWithinAt_left_of_surjOn theorem

 {f : α → β} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s ∈ 𝓝[≤] a) (hfs : SurjOn f s (Iio (f a))) :
  ContinuousWithinAt f (Iic a) a

Full source

/-- If a function `f` is strictly monotone on a left neighborhood of `a` and the image of this
neighborhood under `f` includes `Iio (f a)`, then `f` is continuous at `a` from the left. -/
theorem StrictMonoOn.continuousWithinAt_left_of_surjOn {f : α → β} {s : Set α} {a : α}
    (h_mono : StrictMonoOn f s) (hs : s ∈ 𝓝[≤] a) (hfs : SurjOn f s (Iio (f a))) :
    ContinuousWithinAt f (Iic a) a :=
  h_mono.dual.continuousWithinAt_right_of_surjOn hs hfs

Left Continuity of Strictly Increasing Surjective Functions on Left-Neighborhoods

Informal description

Let $f : \alpha \to \beta$ be a function strictly increasing on a set $s \subseteq \alpha$ that is a left-neighborhood of $a \in \alpha$. If $f$ maps $s$ surjectively onto the left-infinite open interval $(-\infty, f(a))$, then $f$ is continuous at $a$ from the left, i.e., continuous within the interval $(-\infty, a]$ at $a$.

StrictMonoOn.continuousAt_of_exists_between theorem

 {f : α → β} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s ∈ 𝓝 a)
  (hfs_l : ∀ b < f a, ∃ c ∈ s, f c ∈ Ico b (f a)) (hfs_r : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b) : ContinuousAt f a

Full source

/-- If a function `f` is strictly monotone on a neighborhood of `a` and the image of this
neighborhood under `f` meets every interval `[b, f a)`, `b < f a`, and every interval
`(f a, b]`, `b > f a`, then `f` is continuous at `a`. -/
theorem StrictMonoOn.continuousAt_of_exists_between {f : α → β} {s : Set α} {a : α}
    (h_mono : StrictMonoOn f s) (hs : s ∈ 𝓝 a) (hfs_l : ∀ b < f a, ∃ c ∈ s, f c ∈ Ico b (f a))
    (hfs_r : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b) : ContinuousAt f a :=
  continuousAt_iff_continuous_left_right.2
    ⟨h_mono.continuousWithinAt_left_of_exists_between (mem_nhdsWithin_of_mem_nhds hs) hfs_l,
      h_mono.continuousWithinAt_right_of_exists_between (mem_nhdsWithin_of_mem_nhds hs) hfs_r⟩

Continuity of Strictly Increasing Functions via Intermediate Value Property

Informal description

Let $f : \alpha \to \beta$ be a function strictly increasing on a neighborhood $s$ of $a \in \alpha$. Suppose that for every $b < f(a)$, there exists $c \in s$ such that $f(c) \in [b, f(a))$, and for every $b > f(a)$, there exists $c \in s$ such that $f(c) \in (f(a), b]$. Then $f$ is continuous at $a$.

StrictMonoOn.continuousAt_of_closure_image_mem_nhds theorem

 [DenselyOrdered β] {f : α → β} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s ∈ 𝓝 a)
  (hfs : closure (f '' s) ∈ 𝓝 (f a)) : ContinuousAt f a

Full source

/-- If a function `f` with a densely ordered codomain is strictly monotone on a neighborhood of `a`
and the closure of the image of this neighborhood under `f` is a neighborhood of `f a`, then `f` is
continuous at `a`. -/
theorem StrictMonoOn.continuousAt_of_closure_image_mem_nhds [DenselyOrdered β] {f : α → β}
    {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s ∈ 𝓝 a)
    (hfs : closureclosure (f '' s) ∈ 𝓝 (f a)) : ContinuousAt f a :=
  continuousAt_iff_continuous_left_right.2
    ⟨h_mono.continuousWithinAt_left_of_closure_image_mem_nhdsWithin (mem_nhdsWithin_of_mem_nhds hs)
        (mem_nhdsWithin_of_mem_nhds hfs),
      h_mono.continuousWithinAt_right_of_closure_image_mem_nhdsWithin
        (mem_nhdsWithin_of_mem_nhds hs) (mem_nhdsWithin_of_mem_nhds hfs)⟩

Continuity of strictly increasing functions via closure condition

Informal description

Let $\alpha$ and $\beta$ be topological spaces with $\beta$ densely ordered. Let $f : \alpha \to \beta$ be a function that is strictly increasing on a set $s \subseteq \alpha$ which is a neighborhood of $a \in \alpha$. If the closure of the image $f(s)$ is a neighborhood of $f(a)$, then $f$ is continuous at $a$.

StrictMonoOn.continuousAt_of_image_mem_nhds theorem

 [DenselyOrdered β] {f : α → β} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s ∈ 𝓝 a)
  (hfs : f '' s ∈ 𝓝 (f a)) : ContinuousAt f a

Full source

/-- If a function `f` with a densely ordered codomain is strictly monotone on a neighborhood of `a`
and the image of this set under `f` is a neighborhood of `f a`, then `f` is continuous at `a`. -/
theorem StrictMonoOn.continuousAt_of_image_mem_nhds [DenselyOrdered β] {f : α → β} {s : Set α}
    {a : α} (h_mono : StrictMonoOn f s) (hs : s ∈ 𝓝 a) (hfs : f '' sf '' s ∈ 𝓝 (f a)) :
    ContinuousAt f a :=
  h_mono.continuousAt_of_closure_image_mem_nhds hs (mem_of_superset hfs subset_closure)

Continuity of strictly increasing functions via image neighborhood condition

Informal description

Let $\alpha$ and $\beta$ be topological spaces with $\beta$ densely ordered. Let $f : \alpha \to \beta$ be a function that is strictly increasing on a set $s \subseteq \alpha$ which is a neighborhood of $a \in \alpha$. If the image $f(s)$ is a neighborhood of $f(a)$, then $f$ is continuous at $a$.

continuousAt_of_monotoneOn_of_exists_between theorem

 {f : α → β} {s : Set α} {a : α} (h_mono : MonotoneOn f s) (hs : s ∈ 𝓝 a)
  (hfs_l : ∀ b < f a, ∃ c ∈ s, f c ∈ Ioo b (f a)) (hfs_r : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b) : ContinuousAt f a

Full source

/-- If `f` is a monotone function on a neighborhood of `a` and the image of this neighborhood under
`f` meets every interval `(b, f a)`, `b < f a`, and every interval `(f a, b)`, `b > f a`, then `f`
is continuous at `a`. -/
theorem continuousAt_of_monotoneOn_of_exists_between {f : α → β} {s : Set α} {a : α}
    (h_mono : MonotoneOn f s) (hs : s ∈ 𝓝 a) (hfs_l : ∀ b < f a, ∃ c ∈ s, f c ∈ Ioo b (f a))
    (hfs_r : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b) : ContinuousAt f a :=
  continuousAt_iff_continuous_left_right.2
    ⟨continuousWithinAt_left_of_monotoneOn_of_exists_between h_mono (mem_nhdsWithin_of_mem_nhds hs)
        hfs_l,
      continuousWithinAt_right_of_monotoneOn_of_exists_between h_mono
        (mem_nhdsWithin_of_mem_nhds hs) hfs_r⟩

Continuity of Monotone Functions with Intermediate Value Property

Informal description

Let $f : \alpha \to \beta$ be a function that is monotone on a set $s \subseteq \alpha$ which is a neighborhood of $a \in \alpha$. Suppose that for every $b < f(a)$, there exists $c \in s$ such that $f(c) \in (b, f(a))$, and for every $b > f(a)$, there exists $c \in s$ such that $f(c) \in (f(a), b)$. Then $f$ is continuous at $a$.

continuousAt_of_monotoneOn_of_closure_image_mem_nhds theorem

 [DenselyOrdered β] {f : α → β} {s : Set α} {a : α} (h_mono : MonotoneOn f s) (hs : s ∈ 𝓝 a)
  (hfs : closure (f '' s) ∈ 𝓝 (f a)) : ContinuousAt f a

Full source

/-- If a function `f` with a densely ordered codomain is monotone on a neighborhood of `a` and the
closure of the image of this neighborhood under `f` is a neighborhood of `f a`, then `f` is
continuous at `a`. -/
theorem continuousAt_of_monotoneOn_of_closure_image_mem_nhds [DenselyOrdered β] {f : α → β}
    {s : Set α} {a : α} (h_mono : MonotoneOn f s) (hs : s ∈ 𝓝 a)
    (hfs : closureclosure (f '' s) ∈ 𝓝 (f a)) : ContinuousAt f a :=
  continuousAt_iff_continuous_left_right.2
    ⟨continuousWithinAt_left_of_monotoneOn_of_closure_image_mem_nhdsWithin h_mono
        (mem_nhdsWithin_of_mem_nhds hs) (mem_nhdsWithin_of_mem_nhds hfs),
      continuousWithinAt_right_of_monotoneOn_of_closure_image_mem_nhdsWithin h_mono
        (mem_nhdsWithin_of_mem_nhds hs) (mem_nhdsWithin_of_mem_nhds hfs)⟩

Continuity of Monotone Functions via Closure Condition

Informal description

Let $\alpha$ and $\beta$ be topological spaces with $\beta$ densely ordered. Let $f : \alpha \to \beta$ be a function that is monotone on a neighborhood $s$ of $a \in \alpha$. If the closure of the image $f(s)$ is a neighborhood of $f(a)$, then $f$ is continuous at $a$.

continuousAt_of_monotoneOn_of_image_mem_nhds theorem

 [DenselyOrdered β] {f : α → β} {s : Set α} {a : α} (h_mono : MonotoneOn f s) (hs : s ∈ 𝓝 a) (hfs : f '' s ∈ 𝓝 (f a)) :
  ContinuousAt f a

Full source

/-- If a function `f` with a densely ordered codomain is monotone on a neighborhood of `a` and the
image of this neighborhood under `f` is a neighborhood of `f a`, then `f` is continuous at `a`. -/
theorem continuousAt_of_monotoneOn_of_image_mem_nhds [DenselyOrdered β] {f : α → β} {s : Set α}
    {a : α} (h_mono : MonotoneOn f s) (hs : s ∈ 𝓝 a) (hfs : f '' sf '' s ∈ 𝓝 (f a)) : ContinuousAt f a :=
  continuousAt_of_monotoneOn_of_closure_image_mem_nhds h_mono hs
    (mem_of_superset hfs subset_closure)

Continuity of Monotone Functions via Neighborhood Condition

Informal description

Let $\alpha$ and $\beta$ be topological spaces with $\beta$ densely ordered. Let $f : \alpha \to \beta$ be a function that is monotone on a neighborhood $s$ of a point $a \in \alpha$. If the image $f(s)$ is a neighborhood of $f(a)$, then $f$ is continuous at $a$.

Monotone.continuous_of_denseRange theorem

[DenselyOrdered β] {f : α → β} (h_mono : Monotone f) (h_dense : DenseRange f) : Continuous f

Full source

/-- A monotone function with densely ordered codomain and a dense range is continuous. -/
theorem Monotone.continuous_of_denseRange [DenselyOrdered β] {f : α → β} (h_mono : Monotone f)
    (h_dense : DenseRange f) : Continuous f :=
  continuous_iff_continuousAt.mpr fun a =>
    continuousAt_of_monotoneOn_of_closure_image_mem_nhds (fun _ _ _ _ hxy => h_mono hxy)
        univ_mem <|
      by simp only [image_univ, h_dense.closure_eq, univ_mem]

Continuity of Monotone Functions with Dense Range

Informal description

Let $\alpha$ and $\beta$ be topological spaces with $\beta$ densely ordered. If $f : \alpha \to \beta$ is a monotone function with dense range, then $f$ is continuous.

Monotone.continuous_of_surjective theorem

[DenselyOrdered β] {f : α → β} (h_mono : Monotone f) (h_surj : Function.Surjective f) : Continuous f

Full source

/-- A monotone surjective function with a densely ordered codomain is continuous. -/
theorem Monotone.continuous_of_surjective [DenselyOrdered β] {f : α → β} (h_mono : Monotone f)
    (h_surj : Function.Surjective f) : Continuous f :=
  h_mono.continuous_of_denseRange h_surj.denseRange

Continuity of Monotone Surjective Functions on Densely Ordered Codomains

Informal description

Let $\alpha$ and $\beta$ be topological spaces with $\beta$ densely ordered. If $f : \alpha \to \beta$ is a monotone and surjective function, then $f$ is continuous.

OrderIso.continuous theorem

(e : α ≃o β) : Continuous e

Full source

protected theorem continuous (e : α ≃o β) : Continuous e := by
  rw [‹OrderTopology β›.topology_eq_generate_intervals, continuous_generateFrom_iff]
  rintro s ⟨a, rfl | rfl⟩
  · rw [e.preimage_Ioi]
    apply isOpen_lt'
  · rw [e.preimage_Iio]
    apply isOpen_gt'

Continuity of Order Isomorphisms

Informal description

Let $e : \alpha \simeq \beta$ be an order isomorphism between two preordered types $\alpha$ and $\beta$ equipped with their respective order topologies. Then $e$ is a continuous function.

OrderIso.toHomeomorph definition

(e : α ≃o β) : α ≃ₜ β

Full source

/-- An order isomorphism between two linear order `OrderTopology` spaces is a homeomorphism. -/
def toHomeomorph (e : α ≃o β) : α ≃ₜ β :=
  { e with
    continuous_toFun := e.continuous
    continuous_invFun := e.symm.continuous }

Homeomorphism induced by an order isomorphism

Informal description

Given an order isomorphism $e : \alpha \simeq \beta$ between two linear orders equipped with the order topology, the structure `OrderIso.toHomeomorph` promotes $e$ to a homeomorphism, where both $e$ and its inverse $e^{-1}$ are continuous functions.

OrderIso.coe_toHomeomorph theorem

(e : α ≃o β) : ⇑e.toHomeomorph = e

Full source

@[simp]
theorem coe_toHomeomorph (e : α ≃o β) : ⇑e.toHomeomorph = e :=
  rfl

Homeomorphism Function Coincides with Order Isomorphism

Informal description

For any order isomorphism $e : \alpha \simeq \beta$ between two preordered types $\alpha$ and $\beta$ equipped with their respective order topologies, the underlying function of the homeomorphism induced by $e$ is equal to $e$ itself. In other words, the coercion of `e.toHomeomorph` to a function yields the same mapping as $e$.

OrderIso.coe_toHomeomorph_symm theorem

(e : α ≃o β) : ⇑e.toHomeomorph.symm = e.symm

Full source

@[simp]
theorem coe_toHomeomorph_symm (e : α ≃o β) : ⇑e.toHomeomorph.symm = e.symm :=
  rfl

Inverse Homeomorphism of Order Isomorphism Equals Inverse Order Isomorphism

Informal description

For any order isomorphism $e : \alpha \simeq \beta$ between two linear orders with the order topology, the underlying function of the inverse homeomorphism $e.toHomeomorph.symm$ is equal to the underlying function of the inverse order isomorphism $e.symm$.

Tags