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 : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Set.Ioc (f a) b) : ContinuousWithinAt f (Set.Ici a) a

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 : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Set.Ioo (f a) b) : ContinuousWithinAt f (Set.Ici a) a

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))) : ContinuousWithinAt f (Set.Ici a) 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))) : ContinuousWithinAt f (Set.Ici a) 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))) : ContinuousWithinAt f (Set.Ici a) 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))) : ContinuousWithinAt f (Set.Ici a) 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))) : ContinuousWithinAt f (Set.Ici a) 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 : β), b < f a → ∃ c, c ∈ s ∧ f c ∈ Set.Ico b (f a)) : ContinuousWithinAt f (Set.Iic a) 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 : β), b < f a → ∃ c, c ∈ s ∧ f c ∈ Set.Ioo b (f a)) : ContinuousWithinAt f (Set.Iic a) 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))) : ContinuousWithinAt f (Set.Iic a) 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))) : ContinuousWithinAt f (Set.Iic a) 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))) : ContinuousWithinAt f (Set.Iic a) 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))) : ContinuousWithinAt f (Set.Iic a) 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))) : ContinuousWithinAt f (Set.Iic a) 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 : β), b < f a → ∃ c, c ∈ s ∧ f c ∈ Set.Ico b (f a)) (hfs_r : ∀ (b : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Set.Ioc (f a) b) : ContinuousAt f a

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)) : ContinuousAt 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)) : ContinuousAt 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 : β), b < f a → ∃ c, c ∈ s ∧ f c ∈ Set.Ioo b (f a)) (hfs_r : ∀ (b : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Set.Ioo (f a) b) : ContinuousAt f a

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)) : ContinuousAt 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)) : ContinuousAt 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) : Continuous 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) : Continuous 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 β) : Continuous ↑e

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

• OrderIso.toHomeomorph e = Homeomorph.mk e.toEquiv

@[simp]

theorem OrderIso.coe_toHomeomorph {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] [TopologicalSpace α] [TopologicalSpace β] [OrderTopology α] [OrderTopology β] (e : α ≃o β) : ↑(OrderIso.toHomeomorph e) = ↑e

@[simp]

theorem OrderIso.coe_toHomeomorph_symm {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] [TopologicalSpace α] [TopologicalSpace β] [OrderTopology α] [OrderTopology β] (e : α ≃o β) : ↑(Homeomorph.symm (OrderIso.toHomeomorph e)) = ↑(OrderIso.symm e)