chore(topology/algebra/order): add continuous_on.surj_on_of_tendsto (…

…#5502)

* rename `surjective_of_continuous` to `continuous.surjective` and `surjective_of_continuous'` to `continuous.surjective'`;
* add `continuous_on.surj_on_of_tendsto` and `continuous_on.surj_on_of_tendsto'`

src/analysis/special_functions/exp_log.lean

@@ -309,8 +309,8 @@ tendsto_inf.2 ⟨tendsto_exp_at_bot, tendsto_principal.2 $ eventually_of_forall
 /-- `real.exp` as an order isomorphism between `ℝ` and `(0, +∞)`. -/
 def exp_order_iso : ℝ ≃o Ioi (0 : ℝ) :=
 strict_mono.order_iso_of_surjective _ (exp_strict_mono.cod_restrict exp_pos) $
-  surjective_of_continuous (continuous_subtype_mk _ continuous_exp)
-    (by simp only [tendsto_Ioi_at_top, coe_cod_restrict_apply, tendsto_exp_at_top])
+  (continuous_subtype_mk _ continuous_exp).surjective
+    (by simp only [tendsto_Ioi_at_top, subtype.coe_mk, tendsto_exp_at_top])
     (by simp [tendsto_exp_at_bot_nhds_within])
 
 @[simp] lemma coe_exp_order_iso_apply (x : ℝ) : (exp_order_iso x : ℝ) = exp x := rfl

src/data/real/sqrt.lean

@@ -42,8 +42,8 @@ variables {x y : ℝ≥0}
 @[pp_nodot] noncomputable def sqrt : ℝ≥0 ≃o ℝ≥0 :=
 order_iso.symm $ strict_mono.order_iso_of_surjective (λ x, x * x)
   (λ x y h, mul_self_lt_mul_self x.2 h) $
-  surjective_of_continuous (continuous_id.mul continuous_id) tendsto_mul_self_at_top
-    (by simp [order_bot.at_bot_eq])
+  (continuous_id.mul continuous_id).surjective tendsto_mul_self_at_top $
+    by simp [order_bot.at_bot_eq]
 
 lemma sqrt_eq_iff_sqr_eq : sqrt x = y ↔ y * y = x :=
 sqrt.to_equiv.apply_eq_iff_eq_symm_apply.trans eq_comm

src/dynamics/circle/rotation_number/translation_number.lean

@@ -432,8 +432,7 @@ tendsto_at_top_mono f.le_map_of_map_zero $ tendsto_at_top_add_const_left _ _ $
     by simpa [sub_eq_add_neg] using tendsto_at_top_add_const_right _ _ tendsto_id
 
 lemma continuous_iff_surjective : continuous f ↔ function.surjective f :=
-⟨λ h, surjective_of_continuous h f.tendsto_at_top f.tendsto_at_bot,
-  f.monotone.continuous_of_surjective⟩
+⟨λ h, h.surjective f.tendsto_at_top f.tendsto_at_bot, f.monotone.continuous_of_surjective⟩
 
 /-!
 ### Estimates on `(f^n) x`

src/topology/algebra/ordered.lean

@@ -2259,18 +2259,40 @@ lemma intermediate_value_Icc' {a b : α} (hab : a ≤ b) {f : α → δ} (hf : c
 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)
+lemma continuous.surjective {f : α → δ} (hf : continuous f) (h_top : tendsto f at_top at_top)
   (h_bot : tendsto f at_bot at_bot) :
   function.surjective f :=
 λ p, mem_range_of_exists_le_of_exists_ge hf
   (h_bot.eventually (eventually_le_at_bot p)).exists
   (h_top.eventually (eventually_ge_at_top p)).exists
 
 /-- 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)
+lemma continuous.surjective' {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
+@continuous.surjective (order_dual α) _ _ _ _ _ _ _ _ _ hf h_top h_bot
+
+/-- 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 `at_top : filter β` along
+`at_top : filter ↥s`, then the restriction of `f` to `s` is surjective. We formulate the
+conclusion as `surj_on f s univ`. -/
+lemma continuous_on.surj_on_of_tendsto {f : α → β} {s : set α} [ord_connected s]
+  (hs : s.nonempty) (hf : continuous_on f s) (hbot : tendsto (λ x : s, f x) at_bot at_bot)
+  (htop : tendsto (λ x : s, f x) at_top at_top) :
+  surj_on f s univ :=
+by haveI := inhabited_of_nonempty hs.to_subtype;
+  exact (surj_on_iff_surjective.2 $
+    (continuous_on_iff_continuous_restrict.1 hf).surjective htop hbot)
+
+/-- If a function `f : α → β` is continuous on a nonempty interval `s`, its restriction to `s`
+tends to `at_top : filter β` along `at_bot : filter ↥s` and tends to `at_bot : filter β` along
+`at_top : filter ↥s`, then the restriction of `f` to `s` is surjective. We formulate the
+conclusion as `surj_on f s univ`. -/
+lemma continuous_on.surj_on_of_tendsto' {f : α → β} {s : set α} [ord_connected s]
+  (hs : s.nonempty) (hf : continuous_on f s) (hbot : tendsto (λ x : s, f x) at_bot at_top)
+  (htop : tendsto (λ x : s, f x) at_top at_bot) :
+  surj_on f s univ :=
+@continuous_on.surj_on_of_tendsto α (order_dual β) _ _ _ _ _ _ _ _ _ _ hs hf hbot htop
 
 end densely_ordered
 
@@ -3115,7 +3137,7 @@ 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 α β :=
-(h_mono.order_iso_of_surjective f (surjective_of_continuous h_cont h_top h_bot)).to_homeomorph
+(h_mono.order_iso_of_surjective f (h_cont.surjective h_top h_bot)).to_homeomorph
 
 @[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)