feat(topology/algebra/ordered): conditions for a strictly monotone fu…

…nction to be a homeomorphism (#3843)

If a strictly monotone function between linear orders is surjective, it is a homeomorphism.

If a strictly monotone function between conditionally complete linear orders is continuous, and tends to `+∞` at `+∞` and to `-∞` at `-∞`, then it is a homeomorphism.

[Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Order.20topology)

Co-authored by: Yury Kudryashov <urkud@ya.ru>



Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

src/data/set/intervals/basic.lean

@@ -408,8 +408,25 @@ begin
   exact this hmem
 end
 
+lemma Ici_singleton_of_top {a : α} (h_top : ∀ x, x ≤ a) : Ici a = {a} :=
+begin
+  ext,
+  exact ⟨λ h, le_antisymm (h_top _) h, λ h, le_of_eq h.symm⟩,
+end
+
+lemma Iic_singleton_of_bot {a : α} (h_bot : ∀ x, a ≤ x) : Iic a = {a} :=
+@Ici_singleton_of_top (order_dual α) _ a h_bot
+
 end partial_order
 
+section order_top_or_bot
+variables {α : Type u}
+
+@[simp] lemma Ici_top [order_top α] : Ici (⊤ : α) = {⊤} := Ici_singleton_of_top (λ _, le_top)
+@[simp] lemma Ici_bot [order_bot α] : Iic (⊥ : α) = {⊥} := Iic_singleton_of_bot (λ _, bot_le)
+
+end order_top_or_bot
+
 section linear_order
 variables {α : Type u} [linear_order α] {a a₁ a₂ b b₁ b₂ : α}
 

src/data/set/intervals/surj_on.lean

@@ -0,0 +1,114 @@
+/-
+Copyright (c) 2020 Heather Macbeth. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Heather Macbeth
+-/
+import data.set.intervals.basic
+import data.set.function
+
+/-!
+# Monotone surjective functions are surjective on intervals
+
+A monotone surjective function sends any interval in the range onto the interval with corresponding
+endpoints in the range.  This is expressed in this file using `set.surj_on`, and provided for all
+permutations of interval endpoints.
+-/
+
+variables {α : Type*} {β : Type*} [linear_order α] [partial_order β] {f : α → β}
+
+open set function
+
+lemma surj_on_Ioo_of_monotone_surjective
+  (h_mono : monotone f) (h_surj : function.surjective f) (a b : α) :
+  surj_on f (Ioo a b) (Ioo (f a) (f b)) :=
+begin
+  classical,
+  intros p hp,
+  rcases h_surj p with ⟨x, rfl⟩,
+  refine ⟨x, _, rfl⟩,
+  simp only [mem_Ioo],
+  by_contra h,
+  cases not_and_distrib.mp h with ha hb,
+  { exact has_lt.lt.false (lt_of_lt_of_le hp.1 (h_mono (not_lt.mp ha))) },
+  { exact has_lt.lt.false (lt_of_le_of_lt (h_mono (not_lt.mp hb)) hp.2) }
+end
+
+lemma surj_on_Ico_of_monotone_surjective
+  (h_mono : monotone f) (h_surj : function.surjective f) (a b : α) :
+  surj_on f (Ico a b) (Ico (f a) (f b)) :=
+begin
+  rcases lt_or_ge a b with hab|hab,
+  { intros p hp,
+    rcases mem_Ioo_or_eq_left_of_mem_Ico hp with hp'|hp',
+    { rw hp',
+      refine ⟨a, left_mem_Ico.mpr hab, rfl⟩ },
+    { have := surj_on_Ioo_of_monotone_surjective h_mono h_surj a b hp',
+      cases this with x hx,
+      exact ⟨x, Ioo_subset_Ico_self hx.1, hx.2⟩ } },
+  { rw Ico_eq_empty (h_mono hab),
+    exact surj_on_empty f _ },
+end
+
+lemma surj_on_Ioc_of_monotone_surjective
+  (h_mono : monotone f) (h_surj : function.surjective f) (a b : α) :
+  surj_on f (Ioc a b) (Ioc (f a) (f b)) :=
+begin
+  convert @surj_on_Ico_of_monotone_surjective _ _ _ _ _ h_mono.order_dual h_surj b a;
+  simp
+end
+
+-- to see that the hypothesis `a ≤ b` is necessary, consider a constant function
+lemma surj_on_Icc_of_monotone_surjective
+  (h_mono : monotone f) (h_surj : function.surjective f) {a b : α} (hab : a ≤ b) :
+  surj_on f (Icc a b) (Icc (f a) (f b)) :=
+begin
+  rcases lt_or_eq_of_le hab with hab|hab,
+  { intros p hp,
+    rcases mem_Ioo_or_eq_endpoints_of_mem_Icc hp with hp'|⟨hp'|hp'⟩,
+    { rw hp',
+      refine ⟨a, left_mem_Icc.mpr (le_of_lt hab), rfl⟩ },
+    { rw hp',
+      refine ⟨b, right_mem_Icc.mpr (le_of_lt hab), rfl⟩ },
+    { have := surj_on_Ioo_of_monotone_surjective h_mono h_surj a b hp',
+      cases this with x hx,
+      exact ⟨x, Ioo_subset_Icc_self hx.1, hx.2⟩ } },
+  { simp only [hab, Icc_self],
+    intros _ hp,
+    exact ⟨b, mem_singleton _, (mem_singleton_iff.mp hp).symm⟩ }
+end
+
+lemma surj_on_Ioi_of_monotone_surjective
+  (h_mono : monotone f) (h_surj : function.surjective f) (a : α) :
+  surj_on f (Ioi a) (Ioi (f a)) :=
+begin
+  classical,
+  intros p hp,
+  rcases h_surj p with ⟨x, rfl⟩,
+  refine ⟨x, _, rfl⟩,
+  simp only [mem_Ioi],
+  by_contra h,
+  exact has_lt.lt.false (lt_of_lt_of_le hp (h_mono (not_lt.mp h)))
+end
+
+lemma surj_on_Iio_of_monotone_surjective
+  (h_mono : monotone f) (h_surj : function.surjective f) (a : α) :
+  surj_on f (Iio a) (Iio (f a)) :=
+@surj_on_Ioi_of_monotone_surjective _ _ _ _ _ (monotone.order_dual h_mono) h_surj a
+
+lemma surj_on_Ici_of_monotone_surjective
+  (h_mono : monotone f) (h_surj : function.surjective f) (a : α) :
+  surj_on f (Ici a) (Ici (f a)) :=
+begin
+  intros p hp,
+  rw [mem_Ici, le_iff_lt_or_eq] at hp,
+  rcases hp with hp'|hp',
+  { cases (surj_on_Ioi_of_monotone_surjective h_mono h_surj a hp') with x hx,
+    exact ⟨x, Ioi_subset_Ici_self hx.1, hx.2⟩ },
+  { rw ← hp',
+    refine ⟨a, left_mem_Ici, rfl⟩ }
+end
+
+lemma surj_on_Iic_of_monotone_surjective
+  (h_mono : monotone f) (h_surj : function.surjective f) (a : α) :
+  surj_on f (Iic a) (Iic (f a)) :=
+@surj_on_Ici_of_monotone_surjective _ _ _ _ _ (monotone.order_dual h_mono) h_surj a

src/order/basic.lean

@@ -176,6 +176,13 @@ lemma le_iff_le (H : strict_mono f) {a b} :
   f a ≤ f b ↔ a ≤ b :=
 ⟨λ h, le_of_not_gt $ λ h', not_le_of_lt (H h') h,
  λ h, (lt_or_eq_of_le h).elim (λ h', le_of_lt (H h')) (λ h', h' ▸ le_refl _)⟩
+
+lemma top_preimage_top (H : strict_mono f) {a} (h_top : ∀ p, p ≤ f a) (x : α) : x ≤ a :=
+H.le_iff_le.mp (h_top (f x))
+
+lemma bot_preimage_bot (H : strict_mono f) {a} (h_bot : ∀ p, f a ≤ p) (x : α) : a ≤ x :=
+H.le_iff_le.mp (h_bot (f x))
+
 end
 
 protected lemma nat {β} [preorder β] {f : ℕ → β} (h : ∀n, f n < f (n+1)) : strict_mono f :=

src/order/bounded_lattice.lean

@@ -73,6 +73,11 @@ assume ha, hb $ top_unique $ ha ▸ hab
 
 end order_top
 
+lemma strict_mono.top_preimage_top' [linear_order α] [order_top β]
+  {f : α → β} (H : strict_mono f) {a} (h_top : f a = ⊤) (x : α) :
+  x ≤ a :=
+H.top_preimage_top (λ p, by { rw h_top, exact le_top }) x
+
 theorem order_top.ext_top {α} {A B : order_top α}
   (H : ∀ x y : α, (by haveI := A; exact x ≤ y) ↔ x ≤ y) :
   (by haveI := A; exact ⊤ : α) = ⊤ :=
@@ -132,6 +137,11 @@ bot_lt_iff_ne_bot.1 $ lt_of_le_of_lt bot_le h
 
 end order_bot
 
+lemma strict_mono.bot_preimage_bot' [linear_order α] [order_bot β]
+  {f : α → β} (H : strict_mono f) {a} (h_bot : f a = ⊥) (x : α) :
+  a ≤ x :=
+H.bot_preimage_bot (λ p, by { rw h_bot, exact bot_le }) x
+
 theorem order_bot.ext_bot {α} {A B : order_bot α}
   (H : ∀ x y : α, (by haveI := A; exact x ≤ y) ↔ x ≤ y) :
   (by haveI := A; exact ⊥ : α) = ⊥ :=

src/topology/algebra/ordered.lean

@@ -7,6 +7,7 @@ import tactic.tfae
 import order.liminf_limsup
 import data.set.intervals.image_preimage
 import data.set.intervals.ord_connected
+import data.set.intervals.surj_on
 import topology.algebra.group
 import topology.extend_from_subset
 import order.filter.interval
@@ -1181,6 +1182,48 @@ begin
     exact ⟨l, la, subset.trans Ioc_subset_Icc_self as⟩ }
 end
 
+section functions
+variables [topological_space β] [linear_order β] [order_topology β]
+
+/-- If `f : α → β` is strictly monotone and surjective, it is everywhere right-continuous. Superseded
+later in this file by `continuous_of_strict_mono_surjective` (same assumptions). -/
+lemma continuous_right_of_strict_mono_surjective
+  {f : α → β} (h_mono : strict_mono f) (h_surj : function.surjective f) (a : α) :
+  continuous_within_at f (Ici a) a :=
+begin
+  have ha : a ∈ Ici a := left_mem_Ici,
+  intros s hs,
+  by_cases hfa_top : ∃ p, f a < p,
+  { obtain ⟨q, hq, hqs⟩ : ∃ q ∈ Ioi (f a), Ico (f a) q ⊆ s :=
+      exists_Ico_subset_of_mem_nhds hs hfa_top,
+    refine mem_sets_of_superset (mem_map.2 _) hqs,
+    have h_surj_on := surj_on_Ici_of_monotone_surjective h_mono.monotone h_surj a,
+    rcases h_surj_on (Ioi_subset_Ici_self hq) with ⟨x, hx, rfl⟩,
+    rcases eq_or_lt_of_le hx with rfl|hax, { exact (lt_irrefl _ hq).elim },
+    refine mem_sets_of_superset (Ico_mem_nhds_within_Ici (left_mem_Ico.2 hax)) _,
+    intros z hz,
+    exact ⟨h_mono.monotone hz.1, h_mono hz.2⟩ },
+  { push_neg at hfa_top,
+    have ha_top : ∀ x : α, x ≤ a := strict_mono.top_preimage_top h_mono hfa_top,
+    rw [Ici_singleton_of_top ha_top, nhds_within_eq_map_subtype_coe (mem_singleton a),
+      nhds_discrete {x : α // x ∈ {a}}],
+    { exact mem_pure_sets.mpr (mem_of_nhds hs) },
+    { apply_instance } }
+end
+
+/-- If `f : α → β` is strictly monotone and surjective, it is everywhere left-continuous. Superseded
+later in this file by `continuous_of_strict_mono_surjective` (same assumptions). -/
+lemma continuous_left_of_strict_mono_surjective
+  {f : α → β} (h_mono : strict_mono f) (h_surj : function.surjective f) (a : α) :
+  continuous_within_at f (Iic a) a :=
+begin
+  apply @continuous_right_of_strict_mono_surjective (order_dual α) (order_dual β),
+  { exact λ x y hxy, h_mono hxy },
+  { simpa only [dual_Icc] }
+end
+
+end functions
+
 end linear_order
 
 section linear_ordered_ring
@@ -1902,6 +1945,28 @@ lemma intermediate_value_Icc' {a b : α} (hab : a ≤ b) {f : α → β} (hf : c
   Icc (f b) (f a) ⊆ f '' (Icc a b) :=
 is_preconnected_Icc.intermediate_value (right_mem_Icc.2 hab) (left_mem_Icc.2 hab) hf
 
+/-- A continuous function which tendsto `at_top` `at_top` and to `at_bot` `at_bot` is surjective. -/
+lemma surjective_of_continuous {f : α → β} (hf : continuous f) (h_top : tendsto f at_top at_top)
+  (h_bot : tendsto f at_bot at_bot) :
+  function.surjective f :=
+begin
+  intros p,
+  obtain ⟨b, hb⟩ : ∃ b, p ≤ f b,
+    { rcases ((tendsto_at_top_at_top _).mp h_top) p with ⟨b, hb⟩,
+      exact ⟨b, hb b rfl.ge⟩ },
+  obtain ⟨a, hab, ha⟩ : ∃ a, a ≤ b ∧ f a ≤ p,
+  { rcases ((tendsto_at_bot_at_bot _).mp h_bot) p with ⟨x, hx⟩,
+    exact ⟨min x b, min_le_right x b, hx (min x b) (min_le_left x b)⟩ },
+  rcases intermediate_value_Icc hab hf.continuous_on ⟨ha, hb⟩ with ⟨x, _, hx⟩,
+  exact ⟨x, hx⟩
+end
+
+/-- A continuous function which tendsto `at_bot` `at_top` and to `at_top` `at_bot` is surjective. -/
+lemma surjective_of_continuous' {f : α → β} (hf : continuous f) (h_top : tendsto f at_bot at_top)
+  (h_bot : tendsto f at_top at_bot) :
+  function.surjective f :=
+@surjective_of_continuous (order_dual α) β _ _ _ _ _ _ _ _ hf h_top h_bot
+
 end densely_ordered
 
 lemma is_compact.Inf_mem {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :
@@ -2376,3 +2441,74 @@ lemma continuous_at_iff_continuous_left'_right' [topological_space α] [linear_o
   continuous_at f a ↔ continuous_within_at f (Iio a) a ∧ continuous_within_at f (Ioi a) a :=
 by rw [continuous_within_at_Ioi_iff_Ici, continuous_within_at_Iio_iff_Iic,
   continuous_at_iff_continuous_left_right]
+
+section homeomorphisms
+variables [topological_space α] [topological_space β]
+
+section linear_order
+variables [linear_order α] [order_topology α]
+variables [linear_order β] [order_topology β]
+
+/-- If `f : α → β` is strictly monotone and surjective, it is everywhere continuous. -/
+lemma continuous_at_of_strict_mono_surjective
+  {f : α → β} (h_mono : strict_mono f) (h_surj : function.surjective f) (a : α) :
+  continuous_at f a :=
+continuous_at_iff_continuous_left_right.mpr
+  ⟨continuous_left_of_strict_mono_surjective h_mono h_surj a,
+  continuous_right_of_strict_mono_surjective h_mono h_surj a⟩
+
+/-- If `f : α → β` is strictly monotone and surjective, it is continuous. -/
+lemma continuous_of_strict_mono_surjective
+  {f : α → β} (h_mono : strict_mono f) (h_surj : function.surjective f) :
+  continuous f :=
+continuous_iff_continuous_at.mpr (continuous_at_of_strict_mono_surjective h_mono h_surj)
+
+/-- If `f : α ≃ β` is strictly monotone, its inverse is continuous. -/
+lemma continuous_inv_of_strict_mono_equiv (e : α ≃ β) (h_mono : strict_mono e.to_fun) :
+  continuous e.inv_fun :=
+begin
+  have hinv_mono : strict_mono e.inv_fun,
+  { intros x y hxy,
+    rw [← h_mono.lt_iff_lt, e.right_inv, e.right_inv],
+    exact hxy },
+  have hinv_surj : function.surjective e.inv_fun,
+  { intros x,
+    exact ⟨e.to_fun x, e.left_inv x⟩ },
+  exact continuous_of_strict_mono_surjective hinv_mono hinv_surj
+end
+
+/-- If `f : α → β` is strictly monotone and surjective, it is a homeomorphism. -/
+noncomputable def homeomorph_of_strict_mono_surjective
+  (f : α → β) (h_mono : strict_mono f) (h_surj : function.surjective f) :
+  homeomorph α β :=
+{ to_equiv := equiv.of_bijective f ⟨strict_mono.injective h_mono, h_surj⟩,
+  continuous_to_fun := continuous_of_strict_mono_surjective h_mono h_surj,
+  continuous_inv_fun := continuous_inv_of_strict_mono_equiv
+    (equiv.of_bijective f ⟨strict_mono.injective h_mono, h_surj⟩) h_mono }
+
+@[simp] lemma coe_homeomorph_of_strict_mono_surjective
+  (f : α → β) (h_mono : strict_mono f) (h_surj : function.surjective f) :
+  (homeomorph_of_strict_mono_surjective f h_mono h_surj : α → β) = f := rfl
+
+end linear_order
+
+section conditionally_complete_linear_order
+variables [conditionally_complete_linear_order α] [densely_ordered α] [order_topology α]
+variables [conditionally_complete_linear_order β] [order_topology β]
+
+/-- If `f : α → β` is strictly monotone and continuous, and tendsto `at_top` `at_top` and to
+`at_bot` `at_bot`, then it is a homeomorphism. -/
+noncomputable def homeomorph_of_strict_mono_continuous
+  (f : α → β) (h_mono : strict_mono f) (h_cont : continuous f) (h_top : tendsto f at_top at_top)
+  (h_bot : tendsto f at_bot at_bot) :
+  homeomorph α β :=
+homeomorph_of_strict_mono_surjective f h_mono (surjective_of_continuous h_cont h_top h_bot)
+
+@[simp] lemma coe_homeomorph_of_strict_mono_continuous
+  (f : α → β) (h_mono : strict_mono f) (h_cont : continuous f) (h_top : tendsto f at_top at_top)
+  (h_bot : tendsto f at_bot at_bot) :
+  (homeomorph_of_strict_mono_continuous f h_mono h_cont h_top h_bot : α → β) = f := rfl
+
+end conditionally_complete_linear_order
+
+end homeomorphisms