mathlib documentation

topology.algebra.order.monotone_continuity

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 continuous_at_of_monotone_on_of_image_mem_nhds, as well as several similar facts.

We also prove that an order_iso is continuous.

Tags #

continuous, monotone

theorem strict_mono_on.continuous_at_right_of_exists_between {α : Type u_1} {β : Type u_2} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] {f : α → β} {s : set α} {a : α} (h_mono : strict_mono_on f s) (hs : s 𝓝[set.Ici a] a) (hfs : ∀ (b : β), b > f a(∃ (c : α) (H : c s), 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 continuous_at_right_of_monotone_on_of_exists_between {α : Type u_1} {β : Type u_2} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] {f : α → β} {s : set α} {a : α} (h_mono : monotone_on f s) (hs : s 𝓝[set.Ici a] a) (hfs : ∀ (b : β), b > f a(∃ (c : α) (H : c s), 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 continuous_at_right_of_monotone_on_of_closure_image_mem_nhds_within {α : Type u_1} {β : Type u_2} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] [densely_ordered β] {f : α → β} {s : set α} {a : α} (h_mono : monotone_on f s) (hs : s 𝓝[set.Ici a] a) (hfs : closure (f '' s) 𝓝[set.Ici (f a)] 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 continuous_at_right_of_monotone_on_of_image_mem_nhds_within {α : Type u_1} {β : Type u_2} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] [densely_ordered β] {f : α → β} {s : set α} {a : α} (h_mono : monotone_on f s) (hs : s 𝓝[set.Ici a] a) (hfs : f '' s 𝓝[set.Ici (f a)] 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 strict_mono_on.continuous_at_right_of_closure_image_mem_nhds_within {α : Type u_1} {β : Type u_2} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] [densely_ordered β] {f : α → β} {s : set α} {a : α} (h_mono : strict_mono_on f s) (hs : s 𝓝[set.Ici a] a) (hfs : closure (f '' s) 𝓝[set.Ici (f a)] 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 strict_mono_on.continuous_at_right_of_image_mem_nhds_within {α : Type u_1} {β : Type u_2} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] [densely_ordered β] {f : α → β} {s : set α} {a : α} (h_mono : strict_mono_on f s) (hs : s 𝓝[set.Ici a] a) (hfs : f '' s 𝓝[set.Ici (f a)] 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 strict_mono_on.continuous_at_right_of_surj_on {α : Type u_1} {β : Type u_2} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] {f : α → β} {s : set α} {a : α} (h_mono : strict_mono_on f s) (hs : s 𝓝[set.Ici a] a) (hfs : set.surj_on 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 strict_mono_on.continuous_at_left_of_exists_between {α : Type u_1} {β : Type u_2} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] {f : α → β} {s : set α} {a : α} (h_mono : strict_mono_on f s) (hs : s 𝓝[set.Iic a] a) (hfs : ∀ (b : β), b < f a(∃ (c : α) (H : c s), 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 continuous_at_left_of_monotone_on_of_exists_between {α : Type u_1} {β : Type u_2} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] {f : α → β} {s : set α} {a : α} (hf : monotone_on f s) (hs : s 𝓝[set.Iic a] a) (hfs : ∀ (b : β), b < f a(∃ (c : α) (H : c s), 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 continuous_at_left_of_monotone_on_of_closure_image_mem_nhds_within {α : Type u_1} {β : Type u_2} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] [densely_ordered β] {f : α → β} {s : set α} {a : α} (hf : monotone_on f s) (hs : s 𝓝[set.Iic a] a) (hfs : closure (f '' s) 𝓝[set.Iic (f a)] 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 continuous_at_left_of_monotone_on_of_image_mem_nhds_within {α : Type u_1} {β : Type u_2} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] [densely_ordered β] {f : α → β} {s : set α} {a : α} (h_mono : monotone_on f s) (hs : s 𝓝[set.Iic a] a) (hfs : f '' s 𝓝[set.Iic (f a)] 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 strict_mono_on.continuous_at_left_of_closure_image_mem_nhds_within {α : Type u_1} {β : Type u_2} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] [densely_ordered β] {f : α → β} {s : set α} {a : α} (h_mono : strict_mono_on f s) (hs : s 𝓝[set.Iic a] a) (hfs : closure (f '' s) 𝓝[set.Iic (f a)] 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 strict_mono_on.continuous_at_left_of_image_mem_nhds_within {α : Type u_1} {β : Type u_2} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] [densely_ordered β] {f : α → β} {s : set α} {a : α} (h_mono : strict_mono_on f s) (hs : s 𝓝[set.Iic a] a) (hfs : f '' s 𝓝[set.Iic (f a)] 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 strict_mono_on.continuous_at_left_of_surj_on {α : Type u_1} {β : Type u_2} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] {f : α → β} {s : set α} {a : α} (h_mono : strict_mono_on f s) (hs : s 𝓝[set.Iic a] a) (hfs : set.surj_on 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 strict_mono_on.continuous_at_of_exists_between {α : Type u_1} {β : Type u_2} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] {f : α → β} {s : set α} {a : α} (h_mono : strict_mono_on f s) (hs : s 𝓝 a) (hfs_l : ∀ (b : β), b < f a(∃ (c : α) (H : c s), f c set.Ico b (f a))) (hfs_r : ∀ (b : β), b > f a(∃ (c : α) (H : c s), 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 strict_mono_on.continuous_at_of_closure_image_mem_nhds {α : Type u_1} {β : Type u_2} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] [densely_ordered β] {f : α → β} {s : set α} {a : α} (h_mono : strict_mono_on f s) (hs : s 𝓝 a) (hfs : closure (f '' s) 𝓝 (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 strict_mono_on.continuous_at_of_image_mem_nhds {α : Type u_1} {β : Type u_2} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] [densely_ordered β] {f : α → β} {s : set α} {a : α} (h_mono : strict_mono_on f s) (hs : s 𝓝 a) (hfs : f '' s 𝓝 (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 continuous_at_of_monotone_on_of_exists_between {α : Type u_1} {β : Type u_2} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] {f : α → β} {s : set α} {a : α} (h_mono : monotone_on f s) (hs : s 𝓝 a) (hfs_l : ∀ (b : β), b < f a(∃ (c : α) (H : c s), f c set.Ioo b (f a))) (hfs_r : ∀ (b : β), b > f a(∃ (c : α) (H : c s), 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 continuous_at_of_monotone_on_of_closure_image_mem_nhds {α : Type u_1} {β : Type u_2} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] [densely_ordered β] {f : α → β} {s : set α} {a : α} (h_mono : monotone_on f s) (hs : s 𝓝 a) (hfs : closure (f '' s) 𝓝 (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 continuous_at_of_monotone_on_of_image_mem_nhds {α : Type u_1} {β : Type u_2} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] [densely_ordered β] {f : α → β} {s : set α} {a : α} (h_mono : monotone_on f s) (hs : s 𝓝 a) (hfs : f '' s 𝓝 (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_dense_range {α : Type u_1} {β : Type u_2} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] [densely_ordered β] {f : α → β} (h_mono : monotone f) (h_dense : dense_range 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} [linear_order α] [topological_space α] [order_topology α] [linear_order β] [topological_space β] [order_topology β] [densely_ordered β] {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 order_iso is continuous, hence it is a homeomorph. We prove this for an order_iso between to partial orders with order topology.

@[protected]
theorem order_iso.continuous {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] [topological_space α] [topological_space β] [order_topology α] [order_topology β] (e : α ≃o β) :
def order_iso.to_homeomorph {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] [topological_space α] [topological_space β] [order_topology α] [order_topology β] (e : α ≃o β) :
α ≃ₜ β

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

Equations
@[simp]
theorem order_iso.coe_to_homeomorph {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] [topological_space α] [topological_space β] [order_topology α] [order_topology β] (e : α ≃o β) :
@[simp]
theorem order_iso.coe_to_homeomorph_symm {α : Type u_1} {β : Type u_2} [partial_order α] [partial_order β] [topological_space α] [topological_space β] [order_topology α] [order_topology β] (e : α ≃o β) :