Documentation

Mathlib.Topology.Order.MonotoneContinuity

Continuity of monotone functions #

In this file we prove the following fact: if f is a monotone function on a neighborhood of a and the image of this neighborhood is a neighborhood of f a, then f is continuous at a, see continuousWithinAt_of_monotoneOn_of_image_mem_nhds, as well as several similar facts.

We also prove that an OrderIso is continuous.

Tags #

continuous, monotone

theorem StrictMonoOn.continuousWithinAt_right_of_exists_between {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : αβ} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s nhdsWithin a (Set.Ici a)) (hfs : b > f a, cs, f c Set.Ioc (f a) b) :

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 continuousWithinAt_right_of_monotoneOn_of_exists_between {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : αβ} {s : Set α} {a : α} (h_mono : MonotoneOn f s) (hs : s nhdsWithin a (Set.Ici a)) (hfs : b > f a, cs, f c Set.Ioo (f a) b) :

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_closure_image_mem_nhdsWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : αβ} {s : Set α} {a : α} (h_mono : MonotoneOn f s) (hs : s nhdsWithin a (Set.Ici a)) (hfs : closure (f '' s) nhdsWithin (f a) (Set.Ici (f a))) :

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_image_mem_nhdsWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : αβ} {s : Set α} {a : α} (h_mono : MonotoneOn f s) (hs : s nhdsWithin a (Set.Ici a)) (hfs : f '' s nhdsWithin (f a) (Set.Ici (f a))) :

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 StrictMonoOn.continuousWithinAt_right_of_closure_image_mem_nhdsWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : αβ} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s nhdsWithin a (Set.Ici a)) (hfs : closure (f '' s) nhdsWithin (f a) (Set.Ici (f a))) :

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_image_mem_nhdsWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : αβ} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s nhdsWithin a (Set.Ici a)) (hfs : f '' s nhdsWithin (f a) (Set.Ici (f a))) :

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_surjOn {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : αβ} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s nhdsWithin a (Set.Ici a)) (hfs : Set.SurjOn f s (Set.Ioi (f a))) :

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_left_of_exists_between {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : αβ} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s nhdsWithin a (Set.Iic a)) (hfs : b < f a, cs, f c Set.Ico b (f a)) :

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 continuousWithinAt_left_of_monotoneOn_of_exists_between {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : αβ} {s : Set α} {a : α} (hf : MonotoneOn f s) (hs : s nhdsWithin a (Set.Iic a)) (hfs : b < f a, cs, f c Set.Ioo b (f a)) :

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_closure_image_mem_nhdsWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : αβ} {s : Set α} {a : α} (hf : MonotoneOn f s) (hs : s nhdsWithin a (Set.Iic a)) (hfs : closure (f '' s) nhdsWithin (f a) (Set.Iic (f a))) :

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_image_mem_nhdsWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : αβ} {s : Set α} {a : α} (h_mono : MonotoneOn f s) (hs : s nhdsWithin a (Set.Iic a)) (hfs : f '' s nhdsWithin (f a) (Set.Iic (f a))) :

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 StrictMonoOn.continuousWithinAt_left_of_closure_image_mem_nhdsWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : αβ} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s nhdsWithin a (Set.Iic a)) (hfs : closure (f '' s) nhdsWithin (f a) (Set.Iic (f a))) :

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_image_mem_nhdsWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : αβ} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s nhdsWithin a (Set.Iic a)) (hfs : f '' s nhdsWithin (f a) (Set.Iic (f a))) :

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_surjOn {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : αβ} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s nhdsWithin a (Set.Iic a)) (hfs : Set.SurjOn f s (Set.Iio (f a))) :

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.continuousAt_of_exists_between {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : αβ} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s nhds a) (hfs_l : b < f a, cs, f c Set.Ico b (f a)) (hfs_r : b > f a, cs, f c Set.Ioc (f a) b) :

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_closure_image_mem_nhds {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : αβ} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s nhds a) (hfs : closure (f '' s) nhds (f a)) :

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_image_mem_nhds {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : αβ} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s nhds a) (hfs : f '' s nhds (f a)) :

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 continuousAt_of_monotoneOn_of_exists_between {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : αβ} {s : Set α} {a : α} (h_mono : MonotoneOn f s) (hs : s nhds a) (hfs_l : b < f a, cs, f c Set.Ioo b (f a)) (hfs_r : b > f a, cs, f c Set.Ioo (f a) b) :

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_closure_image_mem_nhds {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : αβ} {s : Set α} {a : α} (h_mono : MonotoneOn f s) (hs : s nhds a) (hfs : closure (f '' s) nhds (f a)) :

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_image_mem_nhds {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : αβ} {s : Set α} {a : α} (h_mono : MonotoneOn f s) (hs : s nhds a) (hfs : f '' s nhds (f a)) :

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 Monotone.continuous_of_denseRange {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : αβ} (h_mono : Monotone f) (h_dense : DenseRange f) :

A monotone function with densely ordered codomain and a dense range is continuous.

theorem Monotone.continuous_of_surjective {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : αβ} (h_mono : Monotone f) (h_surj : Function.Surjective f) :

A monotone surjective function with a densely ordered codomain is continuous.

Continuity of order isomorphisms #

In this section we prove that an OrderIso is continuous, hence it is a Homeomorph. We prove this for an OrderIso between to partial orders with order topology.

theorem OrderIso.continuous {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] [TopologicalSpace α] [TopologicalSpace β] [OrderTopology α] [OrderTopology β] (e : α ≃o β) :
def OrderIso.toHomeomorph {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] [TopologicalSpace α] [TopologicalSpace β] [OrderTopology α] [OrderTopology β] (e : α ≃o β) :
α ≃ₜ β

An order isomorphism between two linear order OrderTopology spaces is a homeomorphism.

Equations
  • e.toHomeomorph = { toEquiv := e.toEquiv, continuous_toFun := , continuous_invFun := }
Instances For
    @[simp]
    theorem OrderIso.coe_toHomeomorph {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] [TopologicalSpace α] [TopologicalSpace β] [OrderTopology α] [OrderTopology β] (e : α ≃o β) :
    e.toHomeomorph = e
    @[simp]
    theorem OrderIso.coe_toHomeomorph_symm {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] [TopologicalSpace α] [TopologicalSpace β] [OrderTopology α] [OrderTopology β] (e : α ≃o β) :
    e.toHomeomorph.symm = e.symm