Mathlib.Topology.Order.IntermediateValue

intermediate_value_univ₂ theorem

 [PreconnectedSpace X] {a b : X} {f g : X → α} (hf : Continuous f) (hg : Continuous g) (ha : f a ≤ g a)
  (hb : g b ≤ f b) : ∃ x, f x = g x

Full source

/-- Intermediate value theorem for two functions: if `f` and `g` are two continuous functions
on a preconnected space and `f a ≤ g a` and `g b ≤ f b`, then for some `x` we have `f x = g x`. -/
theorem intermediate_value_univ₂ [PreconnectedSpace X] {a b : X} {f g : X → α} (hf : Continuous f)
    (hg : Continuous g) (ha : f a ≤ g a) (hb : g b ≤ f b) : ∃ x, f x = g x := by
  obtain ⟨x, _, hfg, hgf⟩ : (univuniv ∩ { x | f x ≤ g x ∧ g x ≤ f x }).Nonempty :=
    isPreconnected_closed_iff.1 PreconnectedSpace.isPreconnected_univ _ _ (isClosed_le hf hg)
      (isClosed_le hg hf) (fun _ _ => le_total _ _) ⟨a, trivial, ha⟩ ⟨b, trivial, hb⟩
  exact ⟨x, le_antisymm hfg hgf⟩

Intermediate Value Theorem for Two Functions on a Preconnected Space

Informal description

Let $X$ be a preconnected topological space and $\alpha$ a topological space with an order-closed topology. Given two continuous functions $f, g \colon X \to \alpha$ and points $a, b \in X$ such that $f(a) \leq g(a)$ and $g(b) \leq f(b)$, there exists a point $x \in X$ where $f(x) = g(x)$.

intermediate_value_univ₂_eventually₁ theorem

 [PreconnectedSpace X] {a : X} {l : Filter X} [NeBot l] {f g : X → α} (hf : Continuous f) (hg : Continuous g)
  (ha : f a ≤ g a) (he : g ≤ᶠ[l] f) : ∃ x, f x = g x

Full source

theorem intermediate_value_univ₂_eventually₁ [PreconnectedSpace X] {a : X} {l : Filter X} [NeBot l]
    {f g : X → α} (hf : Continuous f) (hg : Continuous g) (ha : f a ≤ g a) (he : g ≤ᶠ[l] f) :
    ∃ x, f x = g x :=
  let ⟨_, h⟩ := he.exists; intermediate_value_univ₂ hf hg ha h

Intermediate Value Theorem for Two Functions with Filter Condition on a Preconnected Space

Informal description

Let $X$ be a preconnected topological space and $\alpha$ a topological space with an order-closed topology. Given two continuous functions $f, g \colon X \to \alpha$, a point $a \in X$ such that $f(a) \leq g(a)$, and a filter $l$ on $X$ that does not contain the empty set, if $g \leq f$ eventually along $l$, then there exists a point $x \in X$ where $f(x) = g(x)$.

intermediate_value_univ₂_eventually₂ theorem

 [PreconnectedSpace X] {l₁ l₂ : Filter X} [NeBot l₁] [NeBot l₂] {f g : X → α} (hf : Continuous f) (hg : Continuous g)
  (he₁ : f ≤ᶠ[l₁] g) (he₂ : g ≤ᶠ[l₂] f) : ∃ x, f x = g x

Full source

theorem intermediate_value_univ₂_eventually₂ [PreconnectedSpace X] {l₁ l₂ : Filter X} [NeBot l₁]
    [NeBot l₂] {f g : X → α} (hf : Continuous f) (hg : Continuous g) (he₁ : f ≤ᶠ[l₁] g)
    (he₂ : g ≤ᶠ[l₂] f) : ∃ x, f x = g x :=
  let ⟨_, h₁⟩ := he₁.exists
  let ⟨_, h₂⟩ := he₂.exists
  intermediate_value_univ₂ hf hg h₁ h₂

Intermediate Value Theorem for Two Functions with Eventual Comparison on a Preconnected Space

Informal description

Let $X$ be a preconnected topological space and $\alpha$ a topological space with an order-closed topology. Given two continuous functions $f, g \colon X \to \alpha$ and two non-trivial filters $l_1, l_2$ on $X$ such that $f \leq g$ eventually along $l_1$ and $g \leq f$ eventually along $l_2$, there exists a point $x \in X$ where $f(x) = g(x)$.

IsPreconnected.intermediate_value₂ theorem

 {s : Set X} (hs : IsPreconnected s) {a b : X} (ha : a ∈ s) (hb : b ∈ s) {f g : X → α} (hf : ContinuousOn f s)
  (hg : ContinuousOn g s) (ha' : f a ≤ g a) (hb' : g b ≤ f b) : ∃ x ∈ s, f x = g x

Full source

/-- Intermediate value theorem for two functions: if `f` and `g` are two functions continuous
on a preconnected set `s` and for some `a b ∈ s` we have `f a ≤ g a` and `g b ≤ f b`,
then for some `x ∈ s` we have `f x = g x`. -/
theorem IsPreconnected.intermediate_value₂ {s : Set X} (hs : IsPreconnected s) {a b : X}
    (ha : a ∈ s) (hb : b ∈ s) {f g : X → α} (hf : ContinuousOn f s) (hg : ContinuousOn g s)
    (ha' : f a ≤ g a) (hb' : g b ≤ f b) : ∃ x ∈ s, f x = g x :=
  let ⟨x, hx⟩ :=
    @intermediate_value_univ₂ s α _ _ _ _ (Subtype.preconnectedSpace hs) ⟨a, ha⟩ ⟨b, hb⟩ _ _
      (continuousOn_iff_continuous_restrict.1 hf) (continuousOn_iff_continuous_restrict.1 hg) ha'
      hb'
  ⟨x, x.2, hx⟩

Intermediate Value Theorem for Two Continuous Functions on a Preconnected Set

Informal description

Let $X$ be a topological space and $s \subseteq X$ a preconnected subset. For any two continuous functions $f, g \colon X \to \alpha$ (where $\alpha$ has an order-closed topology) and points $a, b \in s$ such that $f(a) \leq g(a)$ and $g(b) \leq f(b)$, there exists a point $x \in s$ where $f(x) = g(x)$.

IsPreconnected.intermediate_value₂_eventually₁ theorem

 {s : Set X} (hs : IsPreconnected s) {a : X} {l : Filter X} (ha : a ∈ s) [NeBot l] (hl : l ≤ 𝓟 s) {f g : X → α}
  (hf : ContinuousOn f s) (hg : ContinuousOn g s) (ha' : f a ≤ g a) (he : g ≤ᶠ[l] f) : ∃ x ∈ s, f x = g x

Full source

theorem IsPreconnected.intermediate_value₂_eventually₁ {s : Set X} (hs : IsPreconnected s) {a : X}
    {l : Filter X} (ha : a ∈ s) [NeBot l] (hl : l ≤ 𝓟 s) {f g : X → α} (hf : ContinuousOn f s)
    (hg : ContinuousOn g s) (ha' : f a ≤ g a) (he : g ≤ᶠ[l] f) : ∃ x ∈ s, f x = g x := by
  rw [continuousOn_iff_continuous_restrict] at hf hg
  obtain ⟨b, h⟩ :=
    @intermediate_value_univ₂_eventually₁ _ _ _ _ _ _ (Subtype.preconnectedSpace hs) ⟨a, ha⟩ _
      (comap_coe_neBot_of_le_principal hl) _ _ hf hg ha' (he.comap _)
  exact ⟨b, b.prop, h⟩

Intermediate Value Theorem for Two Functions with Eventual Comparison on a Preconnected Set

Informal description

Let $X$ be a topological space and $s \subseteq X$ a preconnected subset. Given two continuous functions $f, g \colon X \to \alpha$ (where $\alpha$ has an order-closed topology), a point $a \in s$ such that $f(a) \leq g(a)$, and a filter $l$ on $X$ that does not contain the empty set and is contained in the principal filter of $s$, if $g \leq f$ eventually along $l$, then there exists a point $x \in s$ where $f(x) = g(x)$.

IsPreconnected.intermediate_value₂_eventually₂ theorem

 {s : Set X} (hs : IsPreconnected s) {l₁ l₂ : Filter X} [NeBot l₁] [NeBot l₂] (hl₁ : l₁ ≤ 𝓟 s) (hl₂ : l₂ ≤ 𝓟 s)
  {f g : X → α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) (he₁ : f ≤ᶠ[l₁] g) (he₂ : g ≤ᶠ[l₂] f) :
  ∃ x ∈ s, f x = g x

Full source

theorem IsPreconnected.intermediate_value₂_eventually₂ {s : Set X} (hs : IsPreconnected s)
    {l₁ l₂ : Filter X} [NeBot l₁] [NeBot l₂] (hl₁ : l₁ ≤ 𝓟 s) (hl₂ : l₂ ≤ 𝓟 s) {f g : X → α}
    (hf : ContinuousOn f s) (hg : ContinuousOn g s) (he₁ : f ≤ᶠ[l₁] g) (he₂ : g ≤ᶠ[l₂] f) :
    ∃ x ∈ s, f x = g x := by
  rw [continuousOn_iff_continuous_restrict] at hf hg
  obtain ⟨b, h⟩ :=
    @intermediate_value_univ₂_eventually₂ _ _ _ _ _ _ (Subtype.preconnectedSpace hs) _ _
      (comap_coe_neBot_of_le_principal hl₁) (comap_coe_neBot_of_le_principal hl₂) _ _ hf hg
      (he₁.comap _) (he₂.comap _)
  exact ⟨b, b.prop, h⟩

Intermediate Value Theorem for Two Functions with Eventual Comparison on a Preconnected Set

Informal description

Let $X$ be a topological space and $s \subseteq X$ a preconnected subset. Let $f, g \colon X \to \alpha$ be continuous functions on $s$, where $\alpha$ has an order-closed topology. Suppose there exist two non-trivial filters $l_1, l_2$ on $X$ such that: - $l_1$ and $l_2$ are both finer than the principal filter of $s$, - $f \leq g$ eventually along $l_1$, - $g \leq f$ eventually along $l_2$. Then there exists a point $x \in s$ such that $f(x) = g(x)$.

IsPreconnected.intermediate_value theorem

 {s : Set X} (hs : IsPreconnected s) {a b : X} (ha : a ∈ s) (hb : b ∈ s) {f : X → α} (hf : ContinuousOn f s) :
  Icc (f a) (f b) ⊆ f '' s

Full source

/-- **Intermediate Value Theorem** for continuous functions on connected sets. -/
theorem IsPreconnected.intermediate_value {s : Set X} (hs : IsPreconnected s) {a b : X} (ha : a ∈ s)
    (hb : b ∈ s) {f : X → α} (hf : ContinuousOn f s) : IccIcc (f a) (f b) ⊆ f '' s := fun _x hx =>
  hs.intermediate_value₂ ha hb hf continuousOn_const hx.1 hx.2

Intermediate Value Theorem for Continuous Functions on Preconnected Sets

Informal description

Let $X$ be a topological space and $s \subseteq X$ a preconnected subset. For any continuous function $f \colon X \to \alpha$ (where $\alpha$ has an order-closed topology) and points $a, b \in s$, the closed interval $[f(a), f(b)]$ is contained in the image $f(s)$. In other words, for every $y$ between $f(a)$ and $f(b)$, there exists $x \in s$ such that $f(x) = y$.

IsPreconnected.intermediate_value_Ico theorem

 {s : Set X} (hs : IsPreconnected s) {a : X} {l : Filter X} (ha : a ∈ s) [NeBot l] (hl : l ≤ 𝓟 s) {f : X → α}
  (hf : ContinuousOn f s) {v : α} (ht : Tendsto f l (𝓝 v)) : Ico (f a) v ⊆ f '' s

Full source

theorem IsPreconnected.intermediate_value_Ico {s : Set X} (hs : IsPreconnected s) {a : X}
    {l : Filter X} (ha : a ∈ s) [NeBot l] (hl : l ≤ 𝓟 s) {f : X → α} (hf : ContinuousOn f s) {v : α}
    (ht : Tendsto f l (𝓝 v)) : IcoIco (f a) v ⊆ f '' s := fun _ h =>
  hs.intermediate_value₂_eventually₁ ha hl hf continuousOn_const h.1 (ht.eventually_const_le h.2)

Intermediate Value Theorem for Continuous Functions on Preconnected Sets with Left-Closed Right-Open Interval

Informal description

Let $X$ be a topological space and $s \subseteq X$ a preconnected subset. Let $f \colon X \to \alpha$ be a continuous function on $s$, where $\alpha$ has an order-closed topology. Given a point $a \in s$ and a filter $l$ on $X$ that does not contain the empty set and is contained in the principal filter of $s$, if $f$ tends to $v$ along $l$, then the left-closed right-open interval $[\kern-0.15em[ f(a), v )\kern-0.15em)$ is contained in the image $f(s)$. In other words, for every $y$ such that $f(a) \leq y < v$, there exists $x \in s$ such that $f(x) = y$.

IsPreconnected.intermediate_value_Ioc theorem

 {s : Set X} (hs : IsPreconnected s) {a : X} {l : Filter X} (ha : a ∈ s) [NeBot l] (hl : l ≤ 𝓟 s) {f : X → α}
  (hf : ContinuousOn f s) {v : α} (ht : Tendsto f l (𝓝 v)) : Ioc v (f a) ⊆ f '' s

Full source

theorem IsPreconnected.intermediate_value_Ioc {s : Set X} (hs : IsPreconnected s) {a : X}
    {l : Filter X} (ha : a ∈ s) [NeBot l] (hl : l ≤ 𝓟 s) {f : X → α} (hf : ContinuousOn f s) {v : α}
    (ht : Tendsto f l (𝓝 v)) : IocIoc v (f a) ⊆ f '' s := fun _ h =>
  (hs.intermediate_value₂_eventually₁ ha hl continuousOn_const hf h.2
    (ht.eventually_le_const h.1)).imp fun _ h => h.imp_right Eq.symm

Intermediate Value Theorem for Preconnected Sets with Left-Open Right-Closed Interval

Informal description

Let $X$ be a topological space and $s \subseteq X$ a preconnected subset. Given a continuous function $f \colon X \to \alpha$ (where $\alpha$ has an order-closed topology), a point $a \in s$, and a filter $l$ on $X$ that does not contain the empty set and is contained in the principal filter of $s$, if $f$ tends to $v$ along $l$, then the left-open right-closed interval $(v, f(a)]$ is contained in the image $f(s)$. In other words, for every $y$ such that $v < y \leq f(a)$, there exists $x \in s$ such that $f(x) = y$.

IsPreconnected.intermediate_value_Ioo theorem

 {s : Set X} (hs : IsPreconnected s) {l₁ l₂ : Filter X} [NeBot l₁] [NeBot l₂] (hl₁ : l₁ ≤ 𝓟 s) (hl₂ : l₂ ≤ 𝓟 s)
  {f : X → α} (hf : ContinuousOn f s) {v₁ v₂ : α} (ht₁ : Tendsto f l₁ (𝓝 v₁)) (ht₂ : Tendsto f l₂ (𝓝 v₂)) :
  Ioo v₁ v₂ ⊆ f '' s

Full source

theorem IsPreconnected.intermediate_value_Ioo {s : Set X} (hs : IsPreconnected s) {l₁ l₂ : Filter X}
    [NeBot l₁] [NeBot l₂] (hl₁ : l₁ ≤ 𝓟 s) (hl₂ : l₂ ≤ 𝓟 s) {f : X → α} (hf : ContinuousOn f s)
    {v₁ v₂ : α} (ht₁ : Tendsto f l₁ (𝓝 v₁)) (ht₂ : Tendsto f l₂ (𝓝 v₂)) :
    IooIoo v₁ v₂ ⊆ f '' s := fun _ h =>
  hs.intermediate_value₂_eventually₂ hl₁ hl₂ hf continuousOn_const
    (ht₁.eventually_le_const h.1) (ht₂.eventually_const_le h.2)

Intermediate Value Theorem for Open Intervals on Preconnected Sets

Informal description

Let $X$ be a topological space and $s \subseteq X$ a preconnected subset. Let $f \colon X \to \alpha$ be a continuous function on $s$, where $\alpha$ has an order-closed topology. Given two non-trivial filters $l_1$ and $l_2$ on $X$ that are both finer than the principal filter of $s$, if $f$ tends to $v_1$ along $l_1$ and to $v_2$ along $l_2$, then the open interval $(v_1, v_2)$ is contained in the image $f(s)$. In other words, for every $y \in (v_1, v_2)$, there exists $x \in s$ such that $f(x) = y$.

IsPreconnected.intermediate_value_Ici theorem

 {s : Set X} (hs : IsPreconnected s) {a : X} {l : Filter X} (ha : a ∈ s) [NeBot l] (hl : l ≤ 𝓟 s) {f : X → α}
  (hf : ContinuousOn f s) (ht : Tendsto f l atTop) : Ici (f a) ⊆ f '' s

Full source

theorem IsPreconnected.intermediate_value_Ici {s : Set X} (hs : IsPreconnected s) {a : X}
    {l : Filter X} (ha : a ∈ s) [NeBot l] (hl : l ≤ 𝓟 s) {f : X → α} (hf : ContinuousOn f s)
    (ht : Tendsto f l atTop) : IciIci (f a) ⊆ f '' s := fun y h =>
  hs.intermediate_value₂_eventually₁ ha hl hf continuousOn_const h (tendsto_atTop.1 ht y)

Intermediate Value Theorem for Preconnected Sets with Right-Infinite Image Inclusion

Informal description

Let $X$ be a topological space and $s \subseteq X$ a preconnected subset. Given a continuous function $f \colon X \to \alpha$ (where $\alpha$ has an order-closed topology), a point $a \in s$, and a filter $l$ on $X$ that does not contain the empty set and is contained in the principal filter of $s$, if $f$ tends to infinity along $l$, then the image of $s$ under $f$ contains the closed right-infinite interval $[f(a), \infty)$. In other words, for every $y \geq f(a)$, there exists $x \in s$ such that $f(x) = y$.

IsPreconnected.intermediate_value_Iic theorem

 {s : Set X} (hs : IsPreconnected s) {a : X} {l : Filter X} (ha : a ∈ s) [NeBot l] (hl : l ≤ 𝓟 s) {f : X → α}
  (hf : ContinuousOn f s) (ht : Tendsto f l atBot) : Iic (f a) ⊆ f '' s

Full source

theorem IsPreconnected.intermediate_value_Iic {s : Set X} (hs : IsPreconnected s) {a : X}
    {l : Filter X} (ha : a ∈ s) [NeBot l] (hl : l ≤ 𝓟 s) {f : X → α} (hf : ContinuousOn f s)
    (ht : Tendsto f l atBot) : IicIic (f a) ⊆ f '' s := fun y h =>
  (hs.intermediate_value₂_eventually₁ ha hl continuousOn_const hf h (tendsto_atBot.1 ht y)).imp
    fun _ h => h.imp_right Eq.symm

Intermediate Value Theorem for Left-Infinite Right-Closed Interval with Divergence to $-\infty$

Informal description

Let $X$ be a topological space and $s \subseteq X$ a preconnected subset. Given a continuous function $f \colon X \to \alpha$ (where $\alpha$ has an order-closed topology), a point $a \in s$, and a filter $l$ on $X$ that does not contain the empty set and is contained in the principal filter of $s$, if $f$ tends to $-\infty$ along $l$, then the left-infinite right-closed interval $(-\infty, f(a)]$ is contained in the image of $s$ under $f$.

IsPreconnected.intermediate_value_Ioi theorem

 {s : Set X} (hs : IsPreconnected s) {l₁ l₂ : Filter X} [NeBot l₁] [NeBot l₂] (hl₁ : l₁ ≤ 𝓟 s) (hl₂ : l₂ ≤ 𝓟 s)
  {f : X → α} (hf : ContinuousOn f s) {v : α} (ht₁ : Tendsto f l₁ (𝓝 v)) (ht₂ : Tendsto f l₂ atTop) : Ioi v ⊆ f '' s

Full source

theorem IsPreconnected.intermediate_value_Ioi {s : Set X} (hs : IsPreconnected s) {l₁ l₂ : Filter X}
    [NeBot l₁] [NeBot l₂] (hl₁ : l₁ ≤ 𝓟 s) (hl₂ : l₂ ≤ 𝓟 s) {f : X → α} (hf : ContinuousOn f s)
    {v : α} (ht₁ : Tendsto f l₁ (𝓝 v)) (ht₂ : Tendsto f l₂ atTop) : IoiIoi v ⊆ f '' s := fun y h =>
  hs.intermediate_value₂_eventually₂ hl₁ hl₂ hf continuousOn_const
    (ht₁.eventually_le_const h) (ht₂.eventually_ge_atTop y)

Intermediate Value Theorem for Right-Open Left-Infinite Interval with Convergence to $v$ and Divergence to $+\infty$

Informal description

Let $X$ be a topological space and $s \subseteq X$ a preconnected subset. Let $f \colon X \to \alpha$ be a continuous function on $s$, where $\alpha$ has an order-closed topology. Suppose there exist two non-trivial filters $l_1$ and $l_2$ on $X$ such that: - $l_1$ and $l_2$ are both finer than the principal filter of $s$, - $f$ tends to $v$ along $l_1$, - $f$ tends to $+\infty$ along $l_2$. Then the right-open left-infinite interval $(v, \infty)$ is contained in the image of $s$ under $f$, i.e., for every $y > v$, there exists $x \in s$ such that $f(x) = y$.

IsPreconnected.intermediate_value_Iio theorem

 {s : Set X} (hs : IsPreconnected s) {l₁ l₂ : Filter X} [NeBot l₁] [NeBot l₂] (hl₁ : l₁ ≤ 𝓟 s) (hl₂ : l₂ ≤ 𝓟 s)
  {f : X → α} (hf : ContinuousOn f s) {v : α} (ht₁ : Tendsto f l₁ atBot) (ht₂ : Tendsto f l₂ (𝓝 v)) : Iio v ⊆ f '' s

Full source

theorem IsPreconnected.intermediate_value_Iio {s : Set X} (hs : IsPreconnected s) {l₁ l₂ : Filter X}
    [NeBot l₁] [NeBot l₂] (hl₁ : l₁ ≤ 𝓟 s) (hl₂ : l₂ ≤ 𝓟 s) {f : X → α} (hf : ContinuousOn f s)
    {v : α} (ht₁ : Tendsto f l₁ atBot) (ht₂ : Tendsto f l₂ (𝓝 v)) : IioIio v ⊆ f '' s := fun y h =>
  hs.intermediate_value₂_eventually₂ hl₁ hl₂ hf continuousOn_const (ht₁.eventually_le_atBot y)
    (ht₂.eventually_const_le h)

Intermediate Value Theorem for Left-Infinite Right-Open Interval with Divergence to $-\infty$ and Convergence to $v$

Informal description

Let $X$ be a topological space and $s \subseteq X$ a preconnected subset. Let $f \colon X \to \alpha$ be a continuous function on $s$, where $\alpha$ has an order-closed topology. Suppose there exist two non-trivial filters $l_1$ and $l_2$ on $X$ such that: - $l_1$ and $l_2$ are both finer than the principal filter of $s$, - $f$ tends to $-\infty$ along $l_1$, - $f$ tends to $v$ along $l_2$. Then the left-infinite right-open interval $(-\infty, v)$ is contained in the image of $s$ under $f$, i.e., for every $y < v$, there exists $x \in s$ such that $f(x) = y$.

IsPreconnected.intermediate_value_Iii theorem

 {s : Set X} (hs : IsPreconnected s) {l₁ l₂ : Filter X} [NeBot l₁] [NeBot l₂] (hl₁ : l₁ ≤ 𝓟 s) (hl₂ : l₂ ≤ 𝓟 s)
  {f : X → α} (hf : ContinuousOn f s) (ht₁ : Tendsto f l₁ atBot) (ht₂ : Tendsto f l₂ atTop) : univ ⊆ f '' s

Full source

theorem IsPreconnected.intermediate_value_Iii {s : Set X} (hs : IsPreconnected s) {l₁ l₂ : Filter X}
    [NeBot l₁] [NeBot l₂] (hl₁ : l₁ ≤ 𝓟 s) (hl₂ : l₂ ≤ 𝓟 s) {f : X → α} (hf : ContinuousOn f s)
    (ht₁ : Tendsto f l₁ atBot) (ht₂ : Tendsto f l₂ atTop) : univuniv ⊆ f '' s := fun y _ =>
  hs.intermediate_value₂_eventually₂ hl₁ hl₂ hf continuousOn_const (ht₁.eventually_le_atBot y)
    (ht₂.eventually_ge_atTop y)

Generalized Intermediate Value Theorem for Unbounded Functions on Preconnected Sets

Informal description

Let $X$ be a topological space and $s \subseteq X$ a preconnected subset. Let $f \colon X \to \alpha$ be a continuous function on $s$, where $\alpha$ has an order-closed topology. Suppose there exist two non-trivial filters $l_1$ and $l_2$ on $X$ such that: - $l_1$ and $l_2$ are both finer than the principal filter of $s$, - $f$ tends to $-\infty$ along $l_1$, - $f$ tends to $+\infty$ along $l_2$. Then the range of $f$ on $s$ covers the entire space $\alpha$, i.e., $f(s) = \alpha$.

intermediate_value_univ theorem

[PreconnectedSpace X] (a b : X) {f : X → α} (hf : Continuous f) : Icc (f a) (f b) ⊆ range f

Full source

/-- **Intermediate Value Theorem** for continuous functions on connected spaces. -/
theorem intermediate_value_univ [PreconnectedSpace X] (a b : X) {f : X → α} (hf : Continuous f) :
    IccIcc (f a) (f b) ⊆ range f := fun _ hx => intermediate_value_univ₂ hf continuous_const hx.1 hx.2

Intermediate Value Theorem for Continuous Functions on Preconnected Spaces

Informal description

Let $X$ be a preconnected topological space and $\alpha$ a topological space with an order-closed topology. Given a continuous function $f \colon X \to \alpha$ and points $a, b \in X$, the closed interval $[f(a), f(b)]$ is contained in the range of $f$. In other words, for every $y \in [f(a), f(b)]$, there exists $x \in X$ such that $f(x) = y$.

mem_range_of_exists_le_of_exists_ge theorem

 [PreconnectedSpace X] {c : α} {f : X → α} (hf : Continuous f) (h₁ : ∃ a, f a ≤ c) (h₂ : ∃ b, c ≤ f b) : c ∈ range f

Full source

/-- **Intermediate Value Theorem** for continuous functions on connected spaces. -/
theorem mem_range_of_exists_le_of_exists_ge [PreconnectedSpace X] {c : α} {f : X → α}
    (hf : Continuous f) (h₁ : ∃ a, f a ≤ c) (h₂ : ∃ b, c ≤ f b) : c ∈ range f :=
  let ⟨a, ha⟩ := h₁; let ⟨b, hb⟩ := h₂; intermediate_value_univ a b hf ⟨ha, hb⟩

Intermediate Value Theorem for Continuous Functions on Preconnected Spaces (Existence Version)

Informal description

Let $X$ be a preconnected topological space and $\alpha$ a topological space with an order-closed topology. Given a continuous function $f \colon X \to \alpha$ and a value $c \in \alpha$, if there exist points $a, b \in X$ such that $f(a) \leq c \leq f(b)$, then $c$ is in the range of $f$, i.e., there exists $x \in X$ such that $f(x) = c$.

IsPreconnected.Icc_subset theorem

{s : Set α} (hs : IsPreconnected s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) : Icc a b ⊆ s

Full source

/-- If a preconnected set contains endpoints of an interval, then it includes the whole interval. -/
theorem IsPreconnected.Icc_subset {s : Set α} (hs : IsPreconnected s) {a b : α} (ha : a ∈ s)
    (hb : b ∈ s) : IccIcc a b ⊆ s := by
  simpa only [image_id] using hs.intermediate_value ha hb continuousOn_id

Preconnected Sets Contain Intervals Between Their Points

Informal description

Let $s$ be a preconnected subset of a topological space $\alpha$ with an order-closed topology. For any two points $a, b \in s$, the closed interval $[a, b]$ is contained in $s$. In other words, if $s$ contains the endpoints of an interval, then it contains the entire interval.

IsPreconnected.ordConnected theorem

{s : Set α} (h : IsPreconnected s) : OrdConnected s

Full source

theorem IsPreconnected.ordConnected {s : Set α} (h : IsPreconnected s) : OrdConnected s :=
  ⟨fun _ hx _ hy => h.Icc_subset hx hy⟩

Preconnected Sets are Order Connected

Informal description

Let $s$ be a preconnected subset of a topological space $\alpha$ with an order-closed topology. Then $s$ is order connected, meaning that for any two points $a, b \in s$, the closed interval $[a, b]$ is entirely contained in $s$.

IsConnected.Icc_subset theorem

{s : Set α} (hs : IsConnected s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) : Icc a b ⊆ s

Full source

/-- If a preconnected set contains endpoints of an interval, then it includes the whole interval. -/
theorem IsConnected.Icc_subset {s : Set α} (hs : IsConnected s) {a b : α} (ha : a ∈ s)
    (hb : b ∈ s) : IccIcc a b ⊆ s :=
  hs.2.Icc_subset ha hb

Connected Sets Contain Intervals Between Their Points

Informal description

Let $s$ be a connected subset of a topological space $\alpha$ with an order-closed topology. For any two points $a, b \in s$, the closed interval $[a, b]$ is contained in $s$.

IsConnected.Ioo_csInf_csSup_subset theorem

{s : Set α} (hs : IsConnected s) (hb : BddBelow s) (ha : BddAbove s) : Ioo (sInf s) (sSup s) ⊆ s

Full source

/-- A bounded connected subset of a conditionally complete linear order includes the open interval
`(Inf s, Sup s)`. -/
theorem IsConnected.Ioo_csInf_csSup_subset {s : Set α} (hs : IsConnected s) (hb : BddBelow s)
    (ha : BddAbove s) : IooIoo (sInf s) (sSup s) ⊆ s := fun _x hx =>
  let ⟨_y, ys, hy⟩ := (isGLB_lt_iff (isGLB_csInf hs.nonempty hb)).1 hx.1
  let ⟨_z, zs, hz⟩ := (lt_isLUB_iff (isLUB_csSup hs.nonempty ha)).1 hx.2
  hs.Icc_subset ys zs ⟨hy.le, hz.le⟩

Connected Sets Contain Open Interval Between Infimum and Supremum

Informal description

Let $s$ be a connected subset of a conditionally complete linear order $\alpha$ with the order topology. If $s$ is bounded below and above, then the open interval $(\inf s, \sup s)$ is contained in $s$.

IsPreconnected.Ioi_csInf_subset theorem

{s : Set α} (hs : IsPreconnected s) (hb : BddBelow s) (ha : ¬BddAbove s) : Ioi (sInf s) ⊆ s

Full source

theorem IsPreconnected.Ioi_csInf_subset {s : Set α} (hs : IsPreconnected s) (hb : BddBelow s)
    (ha : ¬BddAbove s) : IoiIoi (sInf s) ⊆ s := fun x hx =>
  have sne : s.Nonempty := nonempty_of_not_bddAbove ha
  let ⟨_y, ys, hy⟩ : ∃ y ∈ s, y < x := (isGLB_lt_iff (isGLB_csInf sne hb)).1 hx
  let ⟨_z, zs, hz⟩ : ∃ z ∈ s, x < z := not_bddAbove_iff.1 ha x
  hs.Icc_subset ys zs ⟨hy.le, hz.le⟩

Preconnected Sets Contain Right-Infinite Intervals Starting at Their Infimum

Informal description

Let $s$ be a preconnected subset of a conditionally complete linear order $\alpha$ with the order topology. If $s$ is bounded below but not bounded above, then the interval $( \inf s, \infty )$ is contained in $s$.

IsPreconnected.Iio_csSup_subset theorem

{s : Set α} (hs : IsPreconnected s) (hb : ¬BddBelow s) (ha : BddAbove s) : Iio (sSup s) ⊆ s

Full source

theorem IsPreconnected.Iio_csSup_subset {s : Set α} (hs : IsPreconnected s) (hb : ¬BddBelow s)
    (ha : BddAbove s) : IioIio (sSup s) ⊆ s :=
  IsPreconnected.Ioi_csInf_subset (α := αᵒᵈ) hs ha hb

Preconnected Sets Contain Left-Infinite Intervals Ending at Their Supremum

Informal description

Let $s$ be a preconnected subset of a conditionally complete linear order $\alpha$ with the order topology. If $s$ is not bounded below but is bounded above, then the interval $(-\infty, \sup s)$ is contained in $s$.

IsPreconnected.mem_intervals theorem

 {s : Set α} (hs : IsPreconnected s) :
  s ∈
    ({Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
        Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} :
      Set (Set α))

Full source

/-- A preconnected set in a conditionally complete linear order is either one of the intervals
`[Inf s, Sup s]`, `[Inf s, Sup s)`, `(Inf s, Sup s]`, `(Inf s, Sup s)`, `[Inf s, +∞)`,
`(Inf s, +∞)`, `(-∞, Sup s]`, `(-∞, Sup s)`, `(-∞, +∞)`, or `∅`. The converse statement requires
`α` to be densely ordered. -/
theorem IsPreconnected.mem_intervals {s : Set α} (hs : IsPreconnected s) :
    s ∈
      ({Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s),
          Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} : Set (Set α)) := by
  rcases s.eq_empty_or_nonempty with (rfl | hne)
  · apply_rules [Or.inr, mem_singleton]
  have hs' : IsConnected s := ⟨hne, hs⟩
  by_cases hb : BddBelow s <;> by_cases ha : BddAbove s
  · refine mem_of_subset_of_mem ?_ <| mem_Icc_Ico_Ioc_Ioo_of_subset_of_subset
      (hs'.Ioo_csInf_csSup_subset hb ha) (subset_Icc_csInf_csSup hb ha)
    simp only [insert_subset_iff, mem_insert_iff, mem_singleton_iff, true_or, or_true,
      singleton_subset_iff, and_self]
  · refine Or.inr <| Or.inr <| Or.inr <| Or.inr ?_
    rcases mem_Ici_Ioi_of_subset_of_subset (hs.Ioi_csInf_subset hb ha) fun x hx ↦
      csInf_le hb hx with hs | hs
    · exact Or.inl hs
    · exact Or.inr (Or.inl hs)
  · iterate 6 apply Or.inr
    rcases mem_Iic_Iio_of_subset_of_subset (hs.Iio_csSup_subset hb ha) fun x hx ↦
      le_csSup ha hx with hs | hs
    · exact Or.inl hs
    · exact Or.inr (Or.inl hs)
  · iterate 8 apply Or.inr
    exact Or.inl (hs.eq_univ_of_unbounded hb ha)

Classification of Preconnected Sets in Conditionally Complete Linear Orders

Informal description

Let $\alpha$ be a conditionally complete linear order with the order topology, and let $s$ be a preconnected subset of $\alpha$. Then $s$ must be one of the following intervals: - The closed interval $[\inf s, \sup s]$, - The left-closed right-open interval $[\inf s, \sup s)$, - The left-open right-closed interval $(\inf s, \sup s]$, - The open interval $(\inf s, \sup s)$, - The left-closed right-infinite interval $[\inf s, \infty)$, - The left-open right-infinite interval $(\inf s, \infty)$, - The left-infinite right-closed interval $(-\infty, \sup s]$, - The left-infinite right-open interval $(-\infty, \sup s)$, - The entire space $\alpha$ (i.e., $(-\infty, \infty)$), - Or the empty set $\emptyset$.

setOf_isPreconnected_subset_of_ordered theorem

 :
  {s : Set α | IsPreconnected s} ⊆
    -- bounded intervals(range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo)) ∪
      -- unbounded intervals and `univ`(range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})

Full source

/-- A preconnected set is either one of the intervals `Icc`, `Ico`, `Ioc`, `Ioo`, `Ici`, `Ioi`,
`Iic`, `Iio`, or `univ`, or `∅`. The converse statement requires `α` to be densely ordered. Though
one can represent `∅` as `(Inf ∅, Inf ∅)`, we include it into the list of possible cases to improve
readability. -/
theorem setOf_isPreconnected_subset_of_ordered :
    { s : Set α | IsPreconnected s }{ s : Set α | IsPreconnected s } ⊆
      -- bounded intervals
      (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo)) ∪
      -- unbounded intervals and `univ`
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}) := by
  intro s hs
  rcases hs.mem_intervals with (hs | hs | hs | hs | hs | hs | hs | hs | hs | hs) <;> rw [hs] <;>
    simp only [union_insert, union_singleton, mem_insert_iff, mem_union, mem_range, Prod.exists,
      uncurry_apply_pair, exists_apply_eq_apply, true_or, or_true, exists_apply_eq_apply2]

Classification of Preconnected Sets in Conditionally Complete Linear Orders

Informal description

Let $\alpha$ be a conditionally complete linear order with the order topology. The collection of all preconnected subsets of $\alpha$ is contained in the union of: - The bounded intervals: all closed intervals $[a, b]$, left-closed right-open intervals $[a, b)$, left-open right-closed intervals $(a, b]$, and open intervals $(a, b)$; - The unbounded intervals: left-closed right-infinite intervals $[a, \infty)$, left-open right-infinite intervals $(a, \infty)$, left-infinite right-closed intervals $(-\infty, b]$, left-infinite right-open intervals $(-\infty, b)$; - The entire space $\alpha$ (i.e., $(-\infty, \infty)$); - The empty set $\emptyset$.

IsClosed.mem_of_ge_of_forall_exists_gt theorem

 {a b : α} {s : Set α} (hs : IsClosed (s ∩ Icc a b)) (ha : a ∈ s) (hab : a ≤ b)
  (hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty) : b ∈ s

Full source

/-- A "continuous induction principle" for a closed interval: if a set `s` meets `[a, b]`
on a closed subset, contains `a`, and the set `s ∩ [a, b)` has no maximal point, then `b ∈ s`. -/
theorem IsClosed.mem_of_ge_of_forall_exists_gt {a b : α} {s : Set α} (hs : IsClosed (s ∩ Icc a b))
    (ha : a ∈ s) (hab : a ≤ b) (hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty) : b ∈ s := by
  let S := s ∩ Icc a b
  replace ha : a ∈ S := ⟨ha, left_mem_Icc.2 hab⟩
  have Sbd : BddAbove S := ⟨b, fun z hz => hz.2.2⟩
  let c := sSup (s ∩ Icc a b)
  have c_mem : c ∈ S := hs.csSup_mem ⟨_, ha⟩ Sbd
  have c_le : c ≤ b := csSup_le ⟨_, ha⟩ fun x hx => hx.2.2
  rcases eq_or_lt_of_le c_le with hc | hc
  · exact hc ▸ c_mem.1
  exfalso
  rcases hgt c ⟨c_mem.1, c_mem.2.1, hc⟩ with ⟨x, xs, cx, xb⟩
  exact not_lt_of_le (le_csSup Sbd ⟨xs, le_trans (le_csSup Sbd ha) (le_of_lt cx), xb⟩) cx

Continuous Induction Principle for Closed Sets in an Interval

Informal description

Let $\alpha$ be a conditionally complete linear order with order topology, and let $s$ be a subset of $\alpha$. Suppose that: 1. The intersection $s \cap [a, b]$ is closed, 2. The point $a$ belongs to $s$, 3. $a \leq b$, and 4. For every $x \in s \cap [a, b)$, there exists a point in $s \cap (x, b]$. Then $b$ belongs to $s$.

IsClosed.Icc_subset_of_forall_exists_gt theorem

 {a b : α} {s : Set α} (hs : IsClosed (s ∩ Icc a b)) (ha : a ∈ s)
  (hgt : ∀ x ∈ s ∩ Ico a b, ∀ y ∈ Ioi x, (s ∩ Ioc x y).Nonempty) : Icc a b ⊆ s

Full source

/-- A "continuous induction principle" for a closed interval: if a set `s` meets `[a, b]`
on a closed subset, contains `a`, and for any `a ≤ x < y ≤ b`, `x ∈ s`, the set `s ∩ (x, y]`
is not empty, then `[a, b] ⊆ s`. -/
theorem IsClosed.Icc_subset_of_forall_exists_gt {a b : α} {s : Set α} (hs : IsClosed (s ∩ Icc a b))
    (ha : a ∈ s) (hgt : ∀ x ∈ s ∩ Ico a b, ∀ y ∈ Ioi x, (s ∩ Ioc x y).Nonempty) : IccIcc a b ⊆ s := by
  intro y hy
  have : IsClosed (s ∩ Icc a y) := by
    suffices s ∩ Icc a y = s ∩ Icc a bs ∩ Icc a b ∩ Icc a y by
      rw [this]
      exact IsClosed.inter hs isClosed_Icc
    rw [inter_assoc]
    congr
    exact (inter_eq_self_of_subset_right <| Icc_subset_Icc_right hy.2).symm
  exact
    IsClosed.mem_of_ge_of_forall_exists_gt this ha hy.1 fun x hx =>
      hgt x ⟨hx.1, Ico_subset_Ico_right hy.2 hx.2⟩ y hx.2.2

Continuous Induction Principle for Closed Sets via Right Neighborhoods

Informal description

Let $\alpha$ be a conditionally complete linear order with the order topology, and let $s$ be a subset of $\alpha$. Suppose that: 1. The intersection $s \cap [a, b]$ is closed, 2. The point $a$ belongs to $s$, and 3. For every $x \in s \cap [a, b)$ and every $y > x$, the intersection $s \cap (x, y]$ is nonempty. Then the closed interval $[a, b]$ is a subset of $s$.

IsClosed.Icc_subset_of_forall_mem_nhdsWithin theorem

 {a b : α} {s : Set α} (hs : IsClosed (s ∩ Icc a b)) (ha : a ∈ s) (hgt : ∀ x ∈ s ∩ Ico a b, s ∈ 𝓝[>] x) : Icc a b ⊆ s

Full source

/-- A "continuous induction principle" for a closed interval: if a set `s` meets `[a, b]`
on a closed subset, contains `a`, and for any `x ∈ s ∩ [a, b)` the set `s` includes some open
neighborhood of `x` within `(x, +∞)`, then `[a, b] ⊆ s`. -/
theorem IsClosed.Icc_subset_of_forall_mem_nhdsWithin {a b : α} {s : Set α}
    (hs : IsClosed (s ∩ Icc a b)) (ha : a ∈ s) (hgt : ∀ x ∈ s ∩ Ico a b, s ∈ 𝓝[>] x) :
    IccIcc a b ⊆ s := by
  apply hs.Icc_subset_of_forall_exists_gt ha
  rintro x ⟨hxs, hxab⟩ y hyxb
  have : s ∩ Ioc x ys ∩ Ioc x y ∈ 𝓝[>] x := inter_mem (hgt x ⟨hxs, hxab⟩) (Ioc_mem_nhdsGT hyxb)
  exact (nhdsGT_neBot_of_exists_gt ⟨b, hxab.2⟩).nonempty_of_mem this

Continuous Induction Principle for Closed Sets via Right Neighborhoods in a Closed Interval

Informal description

Let $\alpha$ be a conditionally complete linear order with the order topology, and let $s$ be a subset of $\alpha$. Suppose that: 1. The intersection $s \cap [a, b]$ is closed, 2. The point $a$ belongs to $s$, and 3. For every $x \in s \cap [a, b)$, there exists a neighborhood to the right of $x$ that is entirely contained in $s$. Then the closed interval $[a, b]$ is a subset of $s$.

isPreconnected_Icc_aux theorem

 (x y : α) (s t : Set α) (hxy : x ≤ y) (hs : IsClosed s) (ht : IsClosed t) (hab : Icc a b ⊆ s ∪ t)
  (hx : x ∈ Icc a b ∩ s) (hy : y ∈ Icc a b ∩ t) : (Icc a b ∩ (s ∩ t)).Nonempty

Full source

theorem isPreconnected_Icc_aux (x y : α) (s t : Set α) (hxy : x ≤ y) (hs : IsClosed s)
    (ht : IsClosed t) (hab : IccIcc a b ⊆ s ∪ t) (hx : x ∈ Icc a b ∩ s) (hy : y ∈ Icc a b ∩ t) :
    (IccIcc a b ∩ (s ∩ t)).Nonempty := by
  have xyab : IccIcc x y ⊆ Icc a b := Icc_subset_Icc hx.1.1 hy.1.2
  by_contra hst
  suffices IccIcc x y ⊆ s from
    hst ⟨y, xyab <| right_mem_Icc.2 hxy, this <| right_mem_Icc.2 hxy, hy.2⟩
  apply (IsClosed.inter hs isClosed_Icc).Icc_subset_of_forall_mem_nhdsWithin hx.2
  rintro z ⟨zs, hz⟩
  have zt : z ∈ tᶜ := fun zt => hst ⟨z, xyab <| Ico_subset_Icc_self hz, zs, zt⟩
  have : tᶜtᶜ ∩ Ioc z ytᶜ ∩ Ioc z y ∈ 𝓝[>] z := by
    rw [← nhdsWithin_Ioc_eq_nhdsGT hz.2]
    exact mem_nhdsWithin.2 ⟨tᶜ, ht.isOpen_compl, zt, Subset.rfl⟩
  apply mem_of_superset this
  have : IocIoc z y ⊆ s ∪ t := fun w hw => hab (xyab ⟨le_trans hz.1 (le_of_lt hw.1), hw.2⟩)
  exact fun w ⟨wt, wzy⟩ => (this wzy).elim id fun h => (wt h).elim

Auxiliary Lemma for Preconnectedness of Closed Intervals via Nonempty Intersection of Closed Sets

Informal description

Let $\alpha$ be a conditionally complete linear order with the order topology, and let $a, b \in \alpha$ with $a \leq b$. Suppose $s$ and $t$ are closed subsets of $\alpha$ such that: 1. The closed interval $[a, b]$ is contained in $s \cup t$, 2. There exist points $x, y \in [a, b]$ with $x \leq y$, $x \in s$, and $y \in t$. Then the intersection $[a, b] \cap (s \cap t)$ is nonempty.

isPreconnected_Icc theorem

: IsPreconnected (Icc a b)

Full source

/-- A closed interval in a densely ordered conditionally complete linear order is preconnected. -/
theorem isPreconnected_Icc : IsPreconnected (Icc a b) :=
  isPreconnected_closed_iff.2
    (by
      rintro s t hs ht hab ⟨x, hx⟩ ⟨y, hy⟩
      -- This used to use `wlog`, but it was causing timeouts.
      rcases le_total x y with h | h
      · exact isPreconnected_Icc_aux x y s t h hs ht hab hx hy
      · rw [inter_comm s t]
        rw [union_comm s t] at hab
        exact isPreconnected_Icc_aux y x t s h ht hs hab hy hx)

Preconnectedness of Closed Intervals in Dense Conditionally Complete Linear Orders

Informal description

In a densely ordered conditionally complete linear order $\alpha$, the closed interval $[a, b]$ is preconnected for any $a, b \in \alpha$.

isPreconnected_uIcc theorem

: IsPreconnected ([[a, b]])

Full source

theorem isPreconnected_uIcc : IsPreconnected ([[a, b]]) :=
  isPreconnected_Icc

Preconnectedness of Unordered Closed Intervals in Dense Conditionally Complete Linear Orders

Informal description

For any two elements $a$ and $b$ in a densely ordered conditionally complete linear order $\alpha$, the unordered closed interval $[a \sqcap b, a \sqcup b]$ is preconnected. This means that the interval, which consists of all elements lying between the infimum and supremum of $a$ and $b$, cannot be partitioned into two disjoint nonempty open subsets.

Set.OrdConnected.isPreconnected theorem

{s : Set α} (h : s.OrdConnected) : IsPreconnected s

Full source

theorem Set.OrdConnected.isPreconnected {s : Set α} (h : s.OrdConnected) : IsPreconnected s :=
  isPreconnected_of_forall_pair fun x hx y hy =>
    ⟨[[x, y]], h.uIcc_subset hx hy, left_mem_uIcc, right_mem_uIcc, isPreconnected_uIcc⟩

Order-Connected Sets are Preconnected

Informal description

If a set $s$ in a linearly ordered type $\alpha$ is order-connected, then $s$ is preconnected in the order topology. That is, for any two points $x, y \in s$, the closed interval $[x, y]$ is contained in $s$, and $s$ cannot be partitioned into two disjoint nonempty open subsets.

isPreconnected_iff_ordConnected theorem

{s : Set α} : IsPreconnected s ↔ OrdConnected s

Full source

theorem isPreconnected_iff_ordConnected {s : Set α} : IsPreconnectedIsPreconnected s ↔ OrdConnected s :=
  ⟨IsPreconnected.ordConnected, Set.OrdConnected.isPreconnected⟩

Equivalence of Preconnectedness and Order Connectedness in Dense Conditionally Complete Linear Orders

Informal description

A subset $s$ of a densely ordered conditionally complete linear order $\alpha$ with the order topology is preconnected if and only if it is order connected. That is, $s$ cannot be partitioned into two disjoint nonempty open subsets if and only if for any two points $x, y \in s$, the closed interval $[x, y]$ is entirely contained in $s$.

isPreconnected_Ici theorem

: IsPreconnected (Ici a)

Full source

theorem isPreconnected_Ici : IsPreconnected (Ici a) :=
  ordConnected_Ici.isPreconnected

Preconnectedness of the Upper Set $[a, \infty)$ in Order Topology

Informal description

For any element $a$ in a conditionally complete linear order $\alpha$ equipped with the order topology, the left-closed right-infinite interval $[a, \infty)$ is a preconnected set.

isPreconnected_Iic theorem

: IsPreconnected (Iic a)

Full source

theorem isPreconnected_Iic : IsPreconnected (Iic a) :=
  ordConnected_Iic.isPreconnected

Preconnectedness of the Lower Set $(-\infty, a]$ in Order Topology

Informal description

For any element $a$ in a conditionally complete linear order $\alpha$ equipped with the order topology, the left-infinite right-closed interval $(-\infty, a]$ is a preconnected set.

isPreconnected_Iio theorem

: IsPreconnected (Iio a)

Full source

theorem isPreconnected_Iio : IsPreconnected (Iio a) :=
  ordConnected_Iio.isPreconnected

Preconnectedness of the Open Interval $(-\infty, a)$ in Order Topology

Informal description

For any element $a$ in a conditionally complete linear order $\alpha$ equipped with the order topology, the left-infinite right-open interval $(-\infty, a) = \{x \in \alpha \mid x < a\}$ is a preconnected set.

isPreconnected_Ioi theorem

: IsPreconnected (Ioi a)

Full source

theorem isPreconnected_Ioi : IsPreconnected (Ioi a) :=
  ordConnected_Ioi.isPreconnected

Preconnectedness of the Open Upper Interval $(a, \infty)$

Informal description

For any element $a$ in a conditionally complete linear order $\alpha$ equipped with the order topology, the left-open right-infinite interval $(a, \infty) = \{x \in \alpha \mid a < x\}$ is a preconnected set.

isPreconnected_Ioo theorem

: IsPreconnected (Ioo a b)

Full source

theorem isPreconnected_Ioo : IsPreconnected (Ioo a b) :=
  ordConnected_Ioo.isPreconnected

Preconnectedness of Open Intervals in Conditionally Complete Linear Orders

Informal description

For any elements $a$ and $b$ in a conditionally complete linear order $\alpha$ equipped with the order topology, the open interval $(a, b) = \{x \in \alpha \mid a < x < b\}$ is a preconnected set.

isPreconnected_Ioc theorem

: IsPreconnected (Ioc a b)

Full source

theorem isPreconnected_Ioc : IsPreconnected (Ioc a b) :=
  ordConnected_Ioc.isPreconnected

Preconnectedness of the Half-Open Interval $(a, b]$ in a Conditionally Complete Linear Order

Informal description

For any elements $a$ and $b$ in a conditionally complete linear order $\alpha$ equipped with the order topology, the left-open right-closed interval $(a, b] = \{x \in \alpha \mid a < x \leq b\}$ is preconnected. This means that $(a, b]$ cannot be partitioned into two disjoint nonempty open subsets in the order topology.

isPreconnected_Ico theorem

: IsPreconnected (Ico a b)

Full source

theorem isPreconnected_Ico : IsPreconnected (Ico a b) :=
  ordConnected_Ico.isPreconnected

Preconnectedness of the Half-Open Interval $[a, b)$ in a Conditionally Complete Linear Order

Informal description

For any elements $a$ and $b$ in a conditionally complete linear order $\alpha$ equipped with the order topology, the left-closed right-open interval $[a, b) = \{x \in \alpha \mid a \leq x < b\}$ is a preconnected set.

isConnected_Ici theorem

: IsConnected (Ici a)

Full source

theorem isConnected_Ici : IsConnected (Ici a) :=
  ⟨nonempty_Ici, isPreconnected_Ici⟩

Connectedness of the Interval $[a, \infty)$ in a Conditionally Complete Linear Order

Informal description

For any element $a$ in a conditionally complete linear order $\alpha$ equipped with the order topology, the left-closed right-infinite interval $[a, \infty)$ is a connected set.

isConnected_Iic theorem

: IsConnected (Iic a)

Full source

theorem isConnected_Iic : IsConnected (Iic a) :=
  ⟨nonempty_Iic, isPreconnected_Iic⟩

Connectedness of the Interval $(-\infty, a]$ in a Conditionally Complete Linear Order

Informal description

For any element $a$ in a conditionally complete linear order $\alpha$ equipped with the order topology, the left-infinite right-closed interval $(-\infty, a]$ is a connected set.

isConnected_Ioi theorem

[NoMaxOrder α] : IsConnected (Ioi a)

Full source

theorem isConnected_Ioi [NoMaxOrder α] : IsConnected (Ioi a) :=
  ⟨nonempty_Ioi, isPreconnected_Ioi⟩

Connectedness of $(a, \infty)$ in a conditionally complete linear order with no maximal element

Informal description

For any element $a$ in a conditionally complete linear order $\alpha$ with no maximal element and equipped with the order topology, the left-open right-infinite interval $(a, \infty)$ is a connected set.

isConnected_Iio theorem

[NoMinOrder α] : IsConnected (Iio a)

Full source

theorem isConnected_Iio [NoMinOrder α] : IsConnected (Iio a) :=
  ⟨nonempty_Iio, isPreconnected_Iio⟩

Connectedness of $(-\infty, a)$ in No-Min-Order Conditionally Complete Linear Order

Informal description

In a conditionally complete linear order $\alpha$ with no minimal element (i.e., for every $a \in \alpha$, there exists $x \in \alpha$ such that $x < a$), the left-infinite right-open interval $(-\infty, a)$ is connected (both topologically connected and order-connected).

isConnected_Icc theorem

(h : a ≤ b) : IsConnected (Icc a b)

Full source

theorem isConnected_Icc (h : a ≤ b) : IsConnected (Icc a b) :=
  ⟨nonempty_Icc.2 h, isPreconnected_Icc⟩

Connectedness of Closed Intervals in Conditionally Complete Linear Orders

Informal description

For any elements $a$ and $b$ in a conditionally complete linear order $\alpha$ equipped with the order topology, if $a \leq b$, then the closed interval $[a, b]$ is connected (both topologically connected and order-connected).

isConnected_Ioo theorem

(h : a < b) : IsConnected (Ioo a b)

Full source

theorem isConnected_Ioo (h : a < b) : IsConnected (Ioo a b) :=
  ⟨nonempty_Ioo.2 h, isPreconnected_Ioo⟩

Connectedness of Open Intervals in Conditionally Complete Linear Orders

Informal description

For any elements $a$ and $b$ in a conditionally complete linear order $\alpha$ equipped with the order topology, if $a < b$, then the open interval $(a, b) = \{x \in \alpha \mid a < x < b\}$ is connected (both topologically connected and order-connected).

isConnected_Ioc theorem

(h : a < b) : IsConnected (Ioc a b)

Full source

theorem isConnected_Ioc (h : a < b) : IsConnected (Ioc a b) :=
  ⟨nonempty_Ioc.2 h, isPreconnected_Ioc⟩

Connectedness of the Interval $(a, b]$ in Conditionally Complete Linear Orders

Informal description

For any elements $a$ and $b$ in a conditionally complete linear order $\alpha$ equipped with the order topology, if $a < b$, then the left-open right-closed interval $(a, b]$ is connected (both topologically connected and order-connected).

isConnected_Ico theorem

(h : a < b) : IsConnected (Ico a b)

Full source

theorem isConnected_Ico (h : a < b) : IsConnected (Ico a b) :=
  ⟨nonempty_Ico.2 h, isPreconnected_Ico⟩

Connectedness of the Interval $[a, b)$ for $a < b$

Informal description

For any elements $a$ and $b$ in a conditionally complete linear order $\alpha$ with the order topology, if $a < b$, then the left-closed right-open interval $[a, b)$ is a connected set.

ordered_connected_space instance

: PreconnectedSpace α

Full source

instance (priority := 100) ordered_connected_space : PreconnectedSpace α :=
  ⟨ordConnected_univ.isPreconnected⟩

Preconnectedness of Conditionally Complete Linear Orders with Order Topology

Informal description

Every conditionally complete linear order with the order topology is a preconnected space.

setOf_isPreconnected_eq_of_ordered theorem

 :
  {s : Set α | IsPreconnected s} =
    -- bounded intervalsrange (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      -- unbounded intervals and `univ`(range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})

Full source

/-- In a dense conditionally complete linear order, the set of preconnected sets is exactly
the set of the intervals `Icc`, `Ico`, `Ioc`, `Ioo`, `Ici`, `Ioi`, `Iic`, `Iio`, `(-∞, +∞)`,
or `∅`. Though one can represent `∅` as `(sInf s, sInf s)`, we include it into the list of
possible cases to improve readability. -/
theorem setOf_isPreconnected_eq_of_ordered :
    { s : Set α | IsPreconnected s } =
      -- bounded intervals
      rangerange (uncurry Icc) ∪ range (uncurry Ico)range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc)range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo)range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      -- unbounded intervals and `univ`
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}) := by
  refine Subset.antisymm setOf_isPreconnected_subset_of_ordered ?_
  simp only [subset_def, forall_mem_range, uncurry, or_imp, forall_and, mem_union,
    mem_setOf_eq, insert_eq, mem_singleton_iff, forall_eq, forall_true_iff, and_true,
    isPreconnected_Icc, isPreconnected_Ico, isPreconnected_Ioc, isPreconnected_Ioo,
    isPreconnected_Ioi, isPreconnected_Iio, isPreconnected_Ici, isPreconnected_Iic,
    isPreconnected_univ, isPreconnected_empty]

Characterization of Preconnected Sets in Densely Ordered Conditionally Complete Linear Orders as Intervals

Informal description

In a densely ordered conditionally complete linear order $\alpha$ with the order topology, a subset $s \subseteq \alpha$ is preconnected if and only if it is one of the following: - A bounded interval: $[a, b]$, $[a, b)$, $(a, b]$, or $(a, b)$ for some $a, b \in \alpha$; - An unbounded interval: $[a, \infty)$, $(a, \infty)$, $(-\infty, b]$, or $(-\infty, b)$ for some $a, b \in \alpha$; - The entire space $\alpha$ (i.e., $(-\infty, \infty)$); - The empty set $\emptyset$.

isTotallyDisconnected_iff_lt theorem

{s : Set α} : IsTotallyDisconnected s ↔ ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∉ s, z ∈ Ioo x y

Full source

/-- This lemmas characterizes when a subset `s` of a densely ordered conditionally complete linear
order is totally disconnected with respect to the order topology: between any two distinct points
of `s` must lie a point not in `s`. -/
lemma isTotallyDisconnected_iff_lt {s : Set α} :
    IsTotallyDisconnectedIsTotallyDisconnected s ↔ ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∉ s, z ∈ Ioo x y := by
  simp only [IsTotallyDisconnected, isPreconnected_iff_ordConnected, ← not_nontrivial_iff,
    nontrivial_iff_exists_lt, not_exists, not_and]
  refine ⟨fun h x hx y hy hxy ↦ ?_, fun h t hts ht x hx y hy hxy ↦ ?_⟩
  · simp_rw [← not_ordConnected_inter_Icc_iff hx hy]
    exact fun hs ↦ h _ inter_subset_left hs _ ⟨hx, le_rfl, hxy.le⟩ _ ⟨hy, hxy.le, le_rfl⟩ hxy
  · obtain ⟨z, h1z, h2z⟩ := h x (hts hx) y (hts hy) hxy
    exact h1z <| hts <| ht.1 hx hy ⟨h2z.1.le, h2z.2.le⟩

Characterization of Totally Disconnected Sets in Densely Ordered Spaces via Missing Intermediate Points

Informal description

A subset $s$ of a densely ordered conditionally complete linear order $\alpha$ with the order topology is totally disconnected if and only if for any two elements $x, y \in s$ with $x < y$, there exists an element $z$ in the open interval $(x, y)$ that does not belong to $s$.

intermediate_value_Icc theorem

{a b : α} (hab : a ≤ b) {f : α → δ} (hf : ContinuousOn f (Icc a b)) : Icc (f a) (f b) ⊆ f '' Icc a b

Full source

/-- **Intermediate Value Theorem** for continuous functions on closed intervals, case
`f a ≤ t ≤ f b`. -/
theorem intermediate_value_Icc {a b : α} (hab : a ≤ b) {f : α → δ} (hf : ContinuousOn f (Icc a b)) :
    IccIcc (f a) (f b) ⊆ f '' Icc a b :=
  isPreconnected_Icc.intermediate_value (left_mem_Icc.2 hab) (right_mem_Icc.2 hab) hf

Intermediate Value Theorem for Continuous Functions on Closed Intervals ($[f(a), f(b)] \subseteq f([a, b])$)

Informal description

Let $\alpha$ and $\delta$ be topological spaces with $\alpha$ having a conditionally complete linear order and order-closed topology. For any $a, b \in \alpha$ with $a \leq b$ and any continuous function $f \colon \alpha \to \delta$ defined on the closed interval $[a, b]$, the image of $f$ on $[a, b]$ contains the closed interval $[f(a), f(b)]$. That is, for every $y \in [f(a), f(b)]$, there exists $x \in [a, b]$ such that $f(x) = y$.

intermediate_value_Icc' theorem

{a b : α} (hab : a ≤ b) {f : α → δ} (hf : ContinuousOn f (Icc a b)) : Icc (f b) (f a) ⊆ f '' Icc a b

Full source

/-- **Intermediate Value Theorem** for continuous functions on closed intervals, case
`f a ≥ t ≥ f b`. -/
theorem intermediate_value_Icc' {a b : α} (hab : a ≤ b) {f : α → δ}
    (hf : ContinuousOn f (Icc a b)) : IccIcc (f b) (f a) ⊆ f '' Icc a b :=
  isPreconnected_Icc.intermediate_value (right_mem_Icc.2 hab) (left_mem_Icc.2 hab) hf

Intermediate Value Theorem for Continuous Functions on Closed Intervals (Decreasing Case)

Informal description

Let $\alpha$ and $\delta$ be conditionally complete linear orders with order-closed topologies. For any continuous function $f \colon \alpha \to \delta$ defined on the closed interval $[a, b]$ (where $a \leq b$), the closed interval $[f(b), f(a)]$ is contained in the image $f([a, b])$. In other words, for every $y$ between $f(b)$ and $f(a)$, there exists $x \in [a, b]$ such that $f(x) = y$.

intermediate_value_uIcc theorem

{a b : α} {f : α → δ} (hf : ContinuousOn f [[a, b]]) : [[f a, f b]] ⊆ f '' uIcc a b

Full source

/-- **Intermediate Value Theorem** for continuous functions on closed intervals, unordered case. -/
theorem intermediate_value_uIcc {a b : α} {f : α → δ} (hf : ContinuousOn f [[a, b]]) :
    [[f a, f b]][[f a, f b]] ⊆ f '' uIcc a b := by
  cases le_total (f a) (f b) <;> simp [*, isPreconnected_uIcc.intermediate_value]

Intermediate Value Theorem for Continuous Functions on Unordered Closed Intervals ($[[f(a), f(b)]] \subseteq f([[a, b]])$)

Informal description

Let $\alpha$ and $\delta$ be conditionally complete linear orders with order-closed topologies. For any continuous function $f \colon \alpha \to \delta$ defined on the unordered closed interval $[[a, b]]$, the image $f([[a, b]])$ contains the unordered closed interval $[[f(a), f(b)]]$. In other words, for every $y$ between $f(a)$ and $f(b)$ (in either order), there exists $x \in [[a, b]]$ such that $f(x) = y$.

exists_mem_uIcc_isFixedPt theorem

 {a b : α} {f : α → α} (hf : ContinuousOn f (uIcc a b)) (ha : a ≤ f a) (hb : f b ≤ b) : ∃ c ∈ [[a, b]], IsFixedPt f c

Full source

/-- If `f : α → α` is continuous on `[[a, b]]`, `a ≤ f a`, and `f b ≤ b`,
then `f` has a fixed point on `[[a, b]]`. -/
theorem exists_mem_uIcc_isFixedPt {a b : α} {f : α → α} (hf : ContinuousOn f (uIcc a b))
    (ha : a ≤ f a) (hb : f b ≤ b) : ∃ c ∈ [[a, b]], IsFixedPt f c :=
  isPreconnected_uIcc.intermediate_value₂ right_mem_uIcc left_mem_uIcc hf continuousOn_id hb ha

Brouwer Fixed-Point Theorem for Continuous Functions on Unordered Closed Intervals

Informal description

Let $\alpha$ be a conditionally complete linear order with the order topology, and let $f \colon \alpha \to \alpha$ be a continuous function on the unordered closed interval $[[a, b]] := [a \sqcap b, a \sqcup b]$. If $a \leq f(a)$ and $f(b) \leq b$, then there exists a point $c \in [[a, b]]$ such that $f(c) = c$.

exists_mem_Icc_isFixedPt theorem

 {a b : α} {f : α → α} (hf : ContinuousOn f (Icc a b)) (hle : a ≤ b) (ha : a ≤ f a) (hb : f b ≤ b) :
  ∃ c ∈ Icc a b, IsFixedPt f c

Full source

/-- If `f : α → α` is continuous on `[a, b]`, `a ≤ b`, `a ≤ f a`, and `f b ≤ b`,
then `f` has a fixed point on `[a, b]`.

In particular, if `[a, b]` is forward-invariant under `f`,
then `f` has a fixed point on `[a, b]`, see `exists_mem_Icc_isFixedPt_of_mapsTo`. -/
theorem exists_mem_Icc_isFixedPt {a b : α} {f : α → α} (hf : ContinuousOn f (Icc a b))
    (hle : a ≤ b) (ha : a ≤ f a) (hb : f b ≤ b) : ∃ c ∈ Icc a b, IsFixedPt f c :=
  isPreconnected_Icc.intermediate_value₂
    (right_mem_Icc.2 hle) (left_mem_Icc.2 hle) hf continuousOn_id hb ha

Brouwer Fixed-Point Theorem for Continuous Functions on Closed Intervals

Informal description

Let $\alpha$ be a conditionally complete linear order with the order topology, and let $f \colon \alpha \to \alpha$ be a continuous function on the closed interval $[a, b]$. If $a \leq b$, $a \leq f(a)$, and $f(b) \leq b$, then there exists a point $c \in [a, b]$ such that $f(c) = c$.

exists_mem_Icc_isFixedPt_of_mapsTo theorem

 {a b : α} {f : α → α} (hf : ContinuousOn f (Icc a b)) (hle : a ≤ b) (hmaps : MapsTo f (Icc a b) (Icc a b)) :
  ∃ c ∈ Icc a b, IsFixedPt f c

Full source

/-- If a closed interval is forward-invariant under a continuous map `f : α → α`,
then this map has a fixed point on this interval. -/
theorem exists_mem_Icc_isFixedPt_of_mapsTo {a b : α} {f : α → α} (hf : ContinuousOn f (Icc a b))
    (hle : a ≤ b) (hmaps : MapsTo f (Icc a b) (Icc a b)) : ∃ c ∈ Icc a b, IsFixedPt f c :=
  exists_mem_Icc_isFixedPt hf hle (hmaps <| left_mem_Icc.2 hle).1 (hmaps <| right_mem_Icc.2 hle).2

Brouwer Fixed-Point Theorem for Continuous Self-Maps on Closed Intervals

Informal description

Let $\alpha$ be a conditionally complete linear order with the order topology, and let $f \colon \alpha \to \alpha$ be a continuous function on the closed interval $[a, b]$. If $a \leq b$ and $f$ maps $[a, b]$ into itself (i.e., $f(x) \in [a, b]$ for all $x \in [a, b]$), then there exists a point $c \in [a, b]$ such that $f(c) = c$.

intermediate_value_Ico theorem

{a b : α} (hab : a ≤ b) {f : α → δ} (hf : ContinuousOn f (Icc a b)) : Ico (f a) (f b) ⊆ f '' Ico a b

Full source

theorem intermediate_value_Ico {a b : α} (hab : a ≤ b) {f : α → δ} (hf : ContinuousOn f (Icc a b)) :
    IcoIco (f a) (f b) ⊆ f '' Ico a b :=
  Or.elim (eq_or_lt_of_le hab) (fun he _ h => absurd h.2 (not_lt_of_le (he ▸ h.1))) fun hlt =>
    @IsPreconnected.intermediate_value_Ico _ _ _ _ _ _ _ isPreconnected_Ico _ _ ⟨refl a, hlt⟩
      (right_nhdsWithin_Ico_neBot hlt) inf_le_right _ (hf.mono Ico_subset_Icc_self) _
      ((hf.continuousWithinAt ⟨hab, refl b⟩).mono Ico_subset_Icc_self)

Intermediate Value Theorem for Continuous Functions on Half-Open Intervals

Informal description

Let $\alpha$ and $\delta$ be types with $\alpha$ equipped with a conditionally complete linear order and order topology. For any $a, b \in \alpha$ with $a \leq b$, and any continuous function $f \colon \alpha \to \delta$ on the closed interval $[a, b]$, the left-closed right-open interval $[f(a), f(b))$ is contained in the image of $f$ restricted to $[a, b)$. In other words, for every $y$ satisfying $f(a) \leq y < f(b)$, there exists $x \in [a, b)$ such that $f(x) = y$.

intermediate_value_Ico' theorem

{a b : α} (hab : a ≤ b) {f : α → δ} (hf : ContinuousOn f (Icc a b)) : Ioc (f b) (f a) ⊆ f '' Ico a b

Full source

theorem intermediate_value_Ico' {a b : α} (hab : a ≤ b) {f : α → δ}
    (hf : ContinuousOn f (Icc a b)) : IocIoc (f b) (f a) ⊆ f '' Ico a b :=
  Or.elim (eq_or_lt_of_le hab) (fun he _ h => absurd h.1 (not_lt_of_le (he ▸ h.2))) fun hlt =>
    @IsPreconnected.intermediate_value_Ioc _ _ _ _ _ _ _ isPreconnected_Ico _ _ ⟨refl a, hlt⟩
      (right_nhdsWithin_Ico_neBot hlt) inf_le_right _ (hf.mono Ico_subset_Icc_self) _
      ((hf.continuousWithinAt ⟨hab, refl b⟩).mono Ico_subset_Icc_self)

Intermediate Value Theorem for Continuous Functions on $[a,b)$ with Image in $(f(b), f(a)]$

Informal description

Let $\alpha$ be a conditionally complete linear order with the order topology, and let $f \colon \alpha \to \delta$ be a continuous function on the closed interval $[a, b]$. If $a \leq b$, then the left-open right-closed interval $(f(b), f(a)]$ is contained in the image of the left-closed right-open interval $[a, b)$ under $f$. In other words, for every $y$ such that $f(b) < y \leq f(a)$, there exists $x \in [a, b)$ such that $f(x) = y$.

intermediate_value_Ioc theorem

{a b : α} (hab : a ≤ b) {f : α → δ} (hf : ContinuousOn f (Icc a b)) : Ioc (f a) (f b) ⊆ f '' Ioc a b

Full source

theorem intermediate_value_Ioc {a b : α} (hab : a ≤ b) {f : α → δ} (hf : ContinuousOn f (Icc a b)) :
    IocIoc (f a) (f b) ⊆ f '' Ioc a b :=
  Or.elim (eq_or_lt_of_le hab) (fun he _ h => absurd h.2 (not_le_of_lt (he ▸ h.1))) fun hlt =>
    @IsPreconnected.intermediate_value_Ioc _ _ _ _ _ _ _ isPreconnected_Ioc _ _ ⟨hlt, refl b⟩
      (left_nhdsWithin_Ioc_neBot hlt) inf_le_right _ (hf.mono Ioc_subset_Icc_self) _
      ((hf.continuousWithinAt ⟨refl a, hab⟩).mono Ioc_subset_Icc_self)

Intermediate Value Theorem for $(f(a), f(b)]$ via $(a, b]$

Informal description

Let $\alpha$ and $\delta$ be conditionally complete linear orders with order-closed topologies. For any $a, b \in \alpha$ with $a \leq b$, if $f \colon \alpha \to \delta$ is continuous on the closed interval $[a, b]$, then the left-open right-closed interval $(f(a), f(b)]$ is contained in the image of the left-open right-closed interval $(a, b]$ under $f$. In other words, for every $y \in \delta$ such that $f(a) < y \leq f(b)$, there exists $x \in (a, b]$ with $f(x) = y$.

intermediate_value_Ioc' theorem

{a b : α} (hab : a ≤ b) {f : α → δ} (hf : ContinuousOn f (Icc a b)) : Ico (f b) (f a) ⊆ f '' Ioc a b

Full source

theorem intermediate_value_Ioc' {a b : α} (hab : a ≤ b) {f : α → δ}
    (hf : ContinuousOn f (Icc a b)) : IcoIco (f b) (f a) ⊆ f '' Ioc a b :=
  Or.elim (eq_or_lt_of_le hab) (fun he _ h => absurd h.1 (not_le_of_lt (he ▸ h.2))) fun hlt =>
    @IsPreconnected.intermediate_value_Ico _ _ _ _ _ _ _ isPreconnected_Ioc _ _ ⟨hlt, refl b⟩
      (left_nhdsWithin_Ioc_neBot hlt) inf_le_right _ (hf.mono Ioc_subset_Icc_self) _
      ((hf.continuousWithinAt ⟨refl a, hab⟩).mono Ioc_subset_Icc_self)

Intermediate Value Theorem for Continuous Functions on $[a,b]$: $[\kern-0.15em[ f(b), f(a) )\kern-0.15em) \subseteq f((a,b])$

Informal description

Let $\alpha$ and $\delta$ be types with $\alpha$ equipped with a conditionally complete linear order and order-closed topology. For any $a, b \in \alpha$ with $a \leq b$, and any continuous function $f \colon \alpha \to \delta$ on the closed interval $[a, b]$, the left-closed right-open interval $[\kern-0.15em[ f(b), f(a) )\kern-0.15em)$ is contained in the image of the left-open right-closed interval $(a, b]$ under $f$. In other words, for every $y$ such that $f(b) \leq y < f(a)$, there exists $x \in (a, b]$ with $f(x) = y$.

intermediate_value_Ioo theorem

{a b : α} (hab : a ≤ b) {f : α → δ} (hf : ContinuousOn f (Icc a b)) : Ioo (f a) (f b) ⊆ f '' Ioo a b

Full source

theorem intermediate_value_Ioo {a b : α} (hab : a ≤ b) {f : α → δ} (hf : ContinuousOn f (Icc a b)) :
    IooIoo (f a) (f b) ⊆ f '' Ioo a b :=
  Or.elim (eq_or_lt_of_le hab) (fun he _ h => absurd h.2 (not_lt_of_lt (he ▸ h.1))) fun hlt =>
    @IsPreconnected.intermediate_value_Ioo _ _ _ _ _ _ _ isPreconnected_Ioo _ _
      (left_nhdsWithin_Ioo_neBot hlt) (right_nhdsWithin_Ioo_neBot hlt) inf_le_right inf_le_right _
      (hf.mono Ioo_subset_Icc_self) _ _
      ((hf.continuousWithinAt ⟨refl a, hab⟩).mono Ioo_subset_Icc_self)
      ((hf.continuousWithinAt ⟨hab, refl b⟩).mono Ioo_subset_Icc_self)

Intermediate Value Theorem for Open Intervals: $(f(a), f(b)) \subseteq f[(a, b)]$

Informal description

Let $\alpha$ and $\delta$ be topological spaces with $\alpha$ having an order-closed topology. For any $a, b \in \alpha$ with $a \leq b$, if $f \colon \alpha \to \delta$ is continuous on the closed interval $[a, b]$, then the open interval $(f(a), f(b))$ is contained in the image of the open interval $(a, b)$ under $f$. In other words, for every $y \in (f(a), f(b))$, there exists $x \in (a, b)$ such that $f(x) = y$.

intermediate_value_Ioo' theorem

{a b : α} (hab : a ≤ b) {f : α → δ} (hf : ContinuousOn f (Icc a b)) : Ioo (f b) (f a) ⊆ f '' Ioo a b

Full source

theorem intermediate_value_Ioo' {a b : α} (hab : a ≤ b) {f : α → δ}
    (hf : ContinuousOn f (Icc a b)) : IooIoo (f b) (f a) ⊆ f '' Ioo a b :=
  Or.elim (eq_or_lt_of_le hab) (fun he _ h => absurd h.1 (not_lt_of_lt (he ▸ h.2))) fun hlt =>
    @IsPreconnected.intermediate_value_Ioo _ _ _ _ _ _ _ isPreconnected_Ioo _ _
      (right_nhdsWithin_Ioo_neBot hlt) (left_nhdsWithin_Ioo_neBot hlt) inf_le_right inf_le_right _
      (hf.mono Ioo_subset_Icc_self) _ _
      ((hf.continuousWithinAt ⟨hab, refl b⟩).mono Ioo_subset_Icc_self)
      ((hf.continuousWithinAt ⟨refl a, hab⟩).mono Ioo_subset_Icc_self)

Intermediate Value Theorem for Open Intervals: $(f(b), f(a)) \subseteq f[(a, b)]$

Informal description

Let $\alpha$ and $\delta$ be topological spaces with $\alpha$ having an order-closed topology. For any $a, b \in \alpha$ with $a \leq b$, if $f \colon \alpha \to \delta$ is continuous on the closed interval $[a, b]$, then the open interval $(f(b), f(a))$ is contained in the image of the open interval $(a, b)$ under $f$. In other words, for every $y \in (f(b), f(a))$, there exists $x \in (a, b)$ such that $f(x) = y$.

ContinuousOn.surjOn_Icc theorem

 {s : Set α} [hs : OrdConnected s] {f : α → δ} (hf : ContinuousOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) :
  SurjOn f s (Icc (f a) (f b))

Full source

/-- **Intermediate value theorem**: if `f` is continuous on an order-connected set `s` and `a`,
`b` are two points of this set, then `f` sends `s` to a superset of `Icc (f x) (f y)`. -/
theorem ContinuousOn.surjOn_Icc {s : Set α} [hs : OrdConnected s] {f : α → δ}
    (hf : ContinuousOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) : SurjOn f s (Icc (f a) (f b)) :=
  hs.isPreconnected.intermediate_value ha hb hf

Intermediate Value Theorem for Continuous Functions on Order-Connected Sets

Informal description

Let $\alpha$ and $\delta$ be topological spaces, where $\alpha$ is equipped with an order-closed topology. Given an order-connected subset $s \subseteq \alpha$, a continuous function $f \colon \alpha \to \delta$ on $s$, and two points $a, b \in s$, the function $f$ maps $s$ onto the closed interval $[f(a), f(b)]$. That is, for every $y \in [f(a), f(b)]$, there exists $x \in s$ such that $f(x) = y$.

ContinuousOn.surjOn_uIcc theorem

 {s : Set α} [hs : OrdConnected s] {f : α → δ} (hf : ContinuousOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) :
  SurjOn f s (uIcc (f a) (f b))

Full source

/-- **Intermediate value theorem**: if `f` is continuous on an order-connected set `s` and `a`,
`b` are two points of this set, then `f` sends `s` to a superset of `[f x, f y]`. -/
theorem ContinuousOn.surjOn_uIcc {s : Set α} [hs : OrdConnected s] {f : α → δ}
    (hf : ContinuousOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) :
    SurjOn f s (uIcc (f a) (f b)) := by
  rcases le_total (f a) (f b) with hab | hab <;> simp [hf.surjOn_Icc, *]

Intermediate Value Theorem for Continuous Functions on Order-Connected Sets (Unordered Interval Version)

Informal description

Let $\alpha$ and $\delta$ be topological spaces, where $\alpha$ is equipped with an order-closed topology. Given an order-connected subset $s \subseteq \alpha$, a continuous function $f \colon \alpha \to \delta$ on $s$, and two points $a, b \in s$, the function $f$ maps $s$ onto the unordered closed interval $[[f(a), f(b)]]$. That is, for every $y$ in the interval between $f(a)$ and $f(b)$ (regardless of their order), there exists $x \in s$ such that $f(x) = y$.

Continuous.surjective theorem

 {f : α → δ} (hf : Continuous f) (h_top : Tendsto f atTop atTop) (h_bot : Tendsto f atBot atBot) : Function.Surjective f

Full source

/-- A continuous function which tendsto `Filter.atTop` along `Filter.atTop` and to `atBot` along
`at_bot` is surjective. -/
theorem Continuous.surjective {f : α → δ} (hf : Continuous f) (h_top : Tendsto f atTop atTop)
    (h_bot : Tendsto f atBot atBot) : Function.Surjective f := fun p =>
  mem_range_of_exists_le_of_exists_ge hf (h_bot.eventually (eventually_le_atBot p)).exists
    (h_top.eventually (eventually_ge_atTop p)).exists

Surjectivity of Continuous Functions with Divergent Limits at Infinity

Informal description

Let $f \colon \alpha \to \delta$ be a continuous function between topological spaces. If $f$ tends to $+\infty$ as $x \to +\infty$ and tends to $-\infty$ as $x \to -\infty$, then $f$ is surjective. In other words, for every $y \in \delta$, there exists $x \in \alpha$ such that $f(x) = y$.

Continuous.surjective' theorem

 {f : α → δ} (hf : Continuous f) (h_top : Tendsto f atBot atTop) (h_bot : Tendsto f atTop atBot) : Function.Surjective f

Full source

/-- A continuous function which tendsto `Filter.atBot` along `Filter.atTop` and to `Filter.atTop`
along `atBot` is surjective. -/
theorem Continuous.surjective' {f : α → δ} (hf : Continuous f) (h_top : Tendsto f atBot atTop)
    (h_bot : Tendsto f atTop atBot) : Function.Surjective f :=
  Continuous.surjective (α := αᵒᵈ) hf h_top h_bot

Surjectivity of Continuous Functions with Antitonic Divergent Limits at Infinity

Informal description

Let $f \colon \alpha \to \delta$ be a continuous function between topological spaces. If $f$ tends to $+\infty$ as $x \to -\infty$ and tends to $-\infty$ as $x \to +\infty$, then $f$ is surjective. That is, for every $y \in \delta$, there exists $x \in \alpha$ such that $f(x) = y$.

ContinuousOn.surjOn_of_tendsto theorem

 {f : α → δ} {s : Set α} [OrdConnected s] (hs : s.Nonempty) (hf : ContinuousOn f s)
  (hbot : Tendsto (fun x : s => f x) atBot atBot) (htop : Tendsto (fun x : s => f x) atTop atTop) : SurjOn f s univ

Full source

/-- If a function `f : α → β` is continuous on a nonempty interval `s`, its restriction to `s`
tends to `at_bot : Filter β` along `at_bot : Filter ↥s` and tends to `Filter.atTop : Filter β` along
`Filter.atTop : Filter ↥s`, then the restriction of `f` to `s` is surjective. We formulate the
conclusion as `Function.surjOn f s Set.univ`. -/
theorem ContinuousOn.surjOn_of_tendsto {f : α → δ} {s : Set α} [OrdConnected s] (hs : s.Nonempty)
    (hf : ContinuousOn f s) (hbot : Tendsto (fun x : s => f x) atBot atBot)
    (htop : Tendsto (fun x : s => f x) atTop atTop) : SurjOn f s univ :=
  haveI := Classical.inhabited_of_nonempty hs.to_subtype
  surjOn_iff_surjective.2 <| hf.restrict.surjective htop hbot

Surjectivity of Continuous Functions on Order-Connected Sets with Divergent Limits

Informal description

Let $\alpha$ and $\delta$ be topological spaces, where $\alpha$ is equipped with a conditionally complete linear order and the order topology. Let $s \subseteq \alpha$ be a nonempty order-connected set, and let $f \colon \alpha \to \delta$ be a function that is continuous on $s$. If the restriction of $f$ to $s$ tends to $-\infty$ as $x \to -\infty$ (along $s$) and tends to $+\infty$ as $x \to +\infty$ (along $s$), then $f$ is surjective onto $\delta$ when restricted to $s$, i.e., for every $y \in \delta$, there exists $x \in s$ such that $f(x) = y$.

ContinuousOn.surjOn_of_tendsto' theorem

 {f : α → δ} {s : Set α} [OrdConnected s] (hs : s.Nonempty) (hf : ContinuousOn f s)
  (hbot : Tendsto (fun x : s => f x) atBot atTop) (htop : Tendsto (fun x : s => f x) atTop atBot) : SurjOn f s univ

Full source

/-- If a function `f : α → β` is continuous on a nonempty interval `s`, its restriction to `s`
tends to `Filter.atTop : Filter β` along `Filter.atBot : Filter ↥s` and tends to
`Filter.atBot : Filter β` along `Filter.atTop : Filter ↥s`, then the restriction of `f` to `s` is
surjective. We formulate the conclusion as `Function.surjOn f s Set.univ`. -/
theorem ContinuousOn.surjOn_of_tendsto' {f : α → δ} {s : Set α} [OrdConnected s] (hs : s.Nonempty)
    (hf : ContinuousOn f s) (hbot : Tendsto (fun x : s => f x) atBot atTop)
    (htop : Tendsto (fun x : s => f x) atTop atBot) : SurjOn f s univ :=
  ContinuousOn.surjOn_of_tendsto (δ := δᵒᵈ) hs hf hbot htop

Surjectivity of Continuous Functions on Order-Connected Sets with Antitonic Divergent Limits

Informal description

Let $\alpha$ be a topological space with a conditionally complete linear order and the order topology, and let $\delta$ be another topological space. Let $s \subseteq \alpha$ be a nonempty order-connected set, and let $f \colon \alpha \to \delta$ be a function that is continuous on $s$. If the restriction of $f$ to $s$ tends to $+\infty$ as $x \to -\infty$ (along $s$) and tends to $-\infty$ as $x \to +\infty$ (along $s$), then $f$ is surjective onto $\delta$ when restricted to $s$, i.e., for every $y \in \delta$, there exists $x \in s$ such that $f(x) = y$.

Continuous.strictMono_of_inj_boundedOrder theorem

[BoundedOrder α] {f : α → δ} (hf_c : Continuous f) (hf : f ⊥ ≤ f ⊤) (hf_i : Injective f) : StrictMono f

Full source

theorem Continuous.strictMono_of_inj_boundedOrder [BoundedOrder α] {f : α → δ}
    (hf_c : Continuous f) (hf : f ⊥ ≤ f ⊤) (hf_i : Injective f) : StrictMono f := by
  intro a b hab
  by_contra! h
  have H : f b < f a := lt_of_le_of_ne h <| hf_i.ne hab.ne'
  by_cases ha : f a ≤ f ⊥
  · obtain ⟨u, hu⟩ := intermediate_value_Ioc le_top hf_c.continuousOn ⟨H.trans_le ha, hf⟩
    have : u = ⊥ := hf_i hu.2
    aesop
  · by_cases hb : f ⊥ < f b
    · obtain ⟨u, hu⟩ := intermediate_value_Ioo bot_le hf_c.continuousOn ⟨hb, H⟩
      rw [hf_i hu.2] at hu
      exact (hab.trans hu.1.2).false
    · push_neg at ha hb
      replace hb : f b < f ⊥ := lt_of_le_of_ne hb <| hf_i.ne (lt_of_lt_of_le' hab bot_le).ne'
      obtain ⟨u, hu⟩ := intermediate_value_Ioo' hab.le hf_c.continuousOn ⟨hb, ha⟩
      have : u = ⊥ := hf_i hu.2
      aesop

Strict monotonicity of continuous injective functions on bounded orders

Informal description

Let $\alpha$ be a bounded order (with top element $\top$ and bottom element $\bot$) and $\delta$ be a topological space. If $f \colon \alpha \to \delta$ is a continuous injective function satisfying $f(\bot) \leq f(\top)$, then $f$ is strictly monotone.

Continuous.strictAnti_of_inj_boundedOrder theorem

[BoundedOrder α] {f : α → δ} (hf_c : Continuous f) (hf : f ⊤ ≤ f ⊥) (hf_i : Injective f) : StrictAnti f

Full source

theorem Continuous.strictAnti_of_inj_boundedOrder [BoundedOrder α] {f : α → δ}
    (hf_c : Continuous f) (hf : f ⊤ ≤ f ⊥) (hf_i : Injective f) : StrictAnti f :=
  hf_c.strictMono_of_inj_boundedOrder (δ := δᵒᵈ) hf hf_i

Strict Antitonicity of Continuous Injective Functions on Bounded Orders

Informal description

Let $\alpha$ be a bounded order (with top element $\top$ and bottom element $\bot$) and $\delta$ be a topological space. If $f \colon \alpha \to \delta$ is a continuous injective function satisfying $f(\top) \leq f(\bot)$, then $f$ is strictly antitone (i.e., strictly decreasing).

Continuous.strictMono_of_inj_boundedOrder' theorem

[BoundedOrder α] {f : α → δ} (hf_c : Continuous f) (hf_i : Injective f) : StrictMono f ∨ StrictAnti f

Full source

theorem Continuous.strictMono_of_inj_boundedOrder' [BoundedOrder α] {f : α → δ}
    (hf_c : Continuous f) (hf_i : Injective f) : StrictMonoStrictMono f ∨ StrictAnti f :=
  (le_total (f ⊥) (f ⊤)).imp
    (hf_c.strictMono_of_inj_boundedOrder · hf_i)
    (hf_c.strictAnti_of_inj_boundedOrder · hf_i)

Strict Monotonicity or Antitonicity of Continuous Injective Functions on Bounded Orders

Informal description

Let $\alpha$ be a bounded order (with top element $\top$ and bottom element $\bot$) and $\delta$ be a topological space. If $f \colon \alpha \to \delta$ is a continuous injective function, then $f$ is either strictly monotone or strictly antitone.

Continuous.strictMonoOn_of_inj_rigidity theorem

 {f : α → δ} (hf_c : Continuous f) (hf_i : Injective f) {a b : α} (hab : a < b) (hf_mono : StrictMonoOn f (Icc a b)) :
  StrictMono f

Full source

/-- Suppose `α` is equipped with a conditionally complete linear dense order and `f : α → δ` is
continuous and injective. Then `f` is strictly monotone (increasing) if
it is strictly monotone (increasing) on some closed interval `[a, b]`. -/
theorem Continuous.strictMonoOn_of_inj_rigidity {f : α → δ}
    (hf_c : Continuous f) (hf_i : Injective f) {a b : α} (hab : a < b)
    (hf_mono : StrictMonoOn f (Icc a b)) : StrictMono f := by
  intro x y hxy
  let s := min a x
  let t := max b y
  have hsa : s ≤ a := min_le_left a x
  have hbt : b ≤ t := le_max_left b y
  have hf_mono_st : StrictMonoOnStrictMonoOn f (Icc s t) ∨ StrictAntiOn f (Icc s t) := by
    have : Fact (s ≤ t) := ⟨hsa.trans <| hbt.trans' hab.le⟩
    have := Continuous.strictMono_of_inj_boundedOrder' (f := Set.restrict (Icc s t) f)
      hf_c.continuousOn.restrict hf_i.injOn.injective
    exact this.imp strictMono_restrict.mp strictAntiOn_iff_strictAnti.mpr
  have (h : StrictAntiOn f (Icc s t)) : False := by
    have : IccIcc a b ⊆ Icc s t := Icc_subset_Icc hsa hbt
    replace : StrictAntiOn f (Icc a b) := StrictAntiOn.mono h this
    replace : IsAntichain (· ≤ ·) (Icc a b) :=
      IsAntichain.of_strictMonoOn_antitoneOn hf_mono this.antitoneOn
    exact this.not_lt (left_mem_Icc.mpr (le_of_lt hab)) (right_mem_Icc.mpr (le_of_lt hab)) hab
  replace hf_mono_st : StrictMonoOn f (Icc s t) := hf_mono_st.resolve_right this
  have hsx : s ≤ x := min_le_right a x
  have hyt : y ≤ t := le_max_right b y
  replace : IccIcc x y ⊆ Icc s t := Icc_subset_Icc hsx hyt
  replace : StrictMonoOn f (Icc x y) := StrictMonoOn.mono hf_mono_st this
  exact this (left_mem_Icc.mpr (le_of_lt hxy)) (right_mem_Icc.mpr (le_of_lt hxy)) hxy

Global Strict Monotonicity from Local Behavior for Continuous Injective Functions on Dense Linear Orders

Informal description

Let $\alpha$ be a conditionally complete linear dense order and $\delta$ be a topological space. Suppose $f \colon \alpha \to \delta$ is a continuous injective function. If $f$ is strictly monotone (increasing) on some closed interval $[a, b]$ with $a < b$, then $f$ is strictly monotone (increasing) on the entire domain $\alpha$.

ContinuousOn.strictMonoOn_of_injOn_Icc theorem

 {a b : α} {f : α → δ} (hab : a ≤ b) (hfab : f a ≤ f b) (hf_c : ContinuousOn f (Icc a b)) (hf_i : InjOn f (Icc a b)) :
  StrictMonoOn f (Icc a b)

Full source

/-- Suppose `f : [a, b] → δ` is
continuous and injective. Then `f` is strictly monotone (increasing) if `f(a) ≤ f(b)`. -/
theorem ContinuousOn.strictMonoOn_of_injOn_Icc {a b : α} {f : α → δ}
    (hab : a ≤ b) (hfab : f a ≤ f b)
    (hf_c : ContinuousOn f (Icc a b)) (hf_i : InjOn f (Icc a b)) :
    StrictMonoOn f (Icc a b) := by
  have : Fact (a ≤ b) := ⟨hab⟩
  refine StrictMono.of_restrict ?_
  set g : Icc a b → δ := Set.restrict (Icc a b) f
  have hgab : g ⊥ ≤ g ⊤ := by aesop
  exact Continuous.strictMono_of_inj_boundedOrder (f := g) hf_c.restrict hgab hf_i.injective

Strict Monotonicity of Continuous Injective Functions on Closed Intervals

Informal description

Let $f \colon [a, b] \to \delta$ be a continuous function on the closed interval $[a, b]$, where $a \leq b$. If $f$ is injective on $[a, b]$ and satisfies $f(a) \leq f(b)$, then $f$ is strictly increasing on $[a, b]$.

ContinuousOn.strictAntiOn_of_injOn_Icc theorem

 {a b : α} {f : α → δ} (hab : a ≤ b) (hfab : f b ≤ f a) (hf_c : ContinuousOn f (Icc a b)) (hf_i : InjOn f (Icc a b)) :
  StrictAntiOn f (Icc a b)

Full source

/-- Suppose `f : [a, b] → δ` is
continuous and injective. Then `f` is strictly antitone (decreasing) if `f(b) ≤ f(a)`. -/
theorem ContinuousOn.strictAntiOn_of_injOn_Icc {a b : α} {f : α → δ}
    (hab : a ≤ b) (hfab : f b ≤ f a)
    (hf_c : ContinuousOn f (Icc a b)) (hf_i : InjOn f (Icc a b)) :
    StrictAntiOn f (Icc a b) := ContinuousOn.strictMonoOn_of_injOn_Icc (δ := δᵒᵈ) hab hfab hf_c hf_i

Strict Antitonicity of Continuous Injective Functions on Closed Intervals

Informal description

Let $f \colon [a, b] \to \delta$ be a continuous function on the closed interval $[a, b]$, where $a \leq b$. If $f$ is injective on $[a, b]$ and satisfies $f(b) \leq f(a)$, then $f$ is strictly decreasing on $[a, b]$.

ContinuousOn.strictMonoOn_of_injOn_Icc' theorem

 {a b : α} {f : α → δ} (hab : a ≤ b) (hf_c : ContinuousOn f (Icc a b)) (hf_i : InjOn f (Icc a b)) :
  StrictMonoOn f (Icc a b) ∨ StrictAntiOn f (Icc a b)

Full source

/-- Suppose `f : [a, b] → δ` is continuous and injective. Then `f` is strictly monotone
or antitone (increasing or decreasing). -/
theorem ContinuousOn.strictMonoOn_of_injOn_Icc' {a b : α} {f : α → δ} (hab : a ≤ b)
    (hf_c : ContinuousOn f (Icc a b)) (hf_i : InjOn f (Icc a b)) :
    StrictMonoOnStrictMonoOn f (Icc a b) ∨ StrictAntiOn f (Icc a b) :=
  (le_total (f a) (f b)).imp
    (ContinuousOn.strictMonoOn_of_injOn_Icc hab · hf_c hf_i)
    (ContinuousOn.strictAntiOn_of_injOn_Icc hab · hf_c hf_i)

Strict Monotonicity of Continuous Injective Functions on Closed Intervals (General Case)

Informal description

Let $f \colon [a, b] \to \delta$ be a continuous function on the closed interval $[a, b]$, where $a \leq b$. If $f$ is injective on $[a, b]$, then $f$ is either strictly increasing or strictly decreasing on $[a, b]$.

Continuous.strictMono_of_inj theorem

{f : α → δ} (hf_c : Continuous f) (hf_i : Injective f) : StrictMono f ∨ StrictAnti f

Full source

/-- Suppose `α` is equipped with a conditionally complete linear dense order and `f : α → δ` is
continuous and injective. Then `f` is strictly monotone or antitone (increasing or decreasing). -/
theorem Continuous.strictMono_of_inj {f : α → δ}
    (hf_c : Continuous f) (hf_i : Injective f) : StrictMonoStrictMono f ∨ StrictAnti f := by
  have H {c d : α} (hcd : c < d) : StrictMonoStrictMono f ∨ StrictAnti f :=
    (hf_c.continuousOn.strictMonoOn_of_injOn_Icc' hcd.le hf_i.injOn).imp
      (hf_c.strictMonoOn_of_inj_rigidity hf_i hcd)
      (hf_c.strictMonoOn_of_inj_rigidity (δ := δᵒᵈ) hf_i hcd)
  by_cases hn : Nonempty α
  · let a : α := Classical.choice ‹_›
    by_cases h : ∃ b : α, a ≠ b
    · choose b hb using h
      by_cases hab : a < b
      · exact H hab
      · push_neg at hab
        have : b < a := by exact Ne.lt_of_le (id (Ne.symm hb)) hab
        exact H this
    · push_neg at h
      haveI : Subsingleton α := ⟨fun c d => Trans.trans (h c).symm (h d)⟩
      exact Or.inl <| Subsingleton.strictMono f
  · aesop

Strict Monotonicity of Continuous Injective Functions on Dense Linear Orders

Informal description

Let $\alpha$ be a conditionally complete linear dense order and $\delta$ be a topological space. If $f \colon \alpha \to \delta$ is a continuous injective function, then $f$ is either strictly increasing or strictly decreasing on $\alpha$.

ContinuousOn.strictMonoOn_of_injOn_Ioo theorem

 {a b : α} {f : α → δ} (hab : a < b) (hf_c : ContinuousOn f (Ioo a b)) (hf_i : InjOn f (Ioo a b)) :
  StrictMonoOn f (Ioo a b) ∨ StrictAntiOn f (Ioo a b)

Full source

/-- Every continuous injective `f : (a, b) → δ` is strictly monotone
or antitone (increasing or decreasing). -/
theorem ContinuousOn.strictMonoOn_of_injOn_Ioo {a b : α} {f : α → δ} (hab : a < b)
    (hf_c : ContinuousOn f (Ioo a b)) (hf_i : InjOn f (Ioo a b)) :
    StrictMonoOnStrictMonoOn f (Ioo a b) ∨ StrictAntiOn f (Ioo a b) := by
  haveI : Inhabited (Ioo a b) := Classical.inhabited_of_nonempty (nonempty_Ioo_subtype hab)
  let g : Ioo a b → δ := Set.restrict (Ioo a b) f
  have : StrictMonoStrictMono g ∨ StrictAnti g :=
    Continuous.strictMono_of_inj hf_c.restrict hf_i.injective
  exact this.imp strictMono_restrict.mp strictAntiOn_iff_strictAnti.mpr

Strict Monotonicity of Continuous Injective Functions on Open Intervals

Informal description

Let $a < b$ be real numbers and $f \colon (a, b) \to \delta$ be a continuous injective function on the open interval $(a, b)$. Then $f$ is either strictly increasing or strictly decreasing on $(a, b)$.

Mathlib.Topology.Order.IntermediateValue

Main results

Miscellaneous facts

Tags