From 49c684125cdf421b3cff0bb17dd59376a3cc613f Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Sun, 24 Oct 2021 03:33:37 +0000 Subject: [PATCH] chore(topology): generalize `real.image_Icc` etc (#9784) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * add lemmas about `Ici`/`Iic`/`Icc` in `α × β`; * introduce a typeclass for `is_compact_Icc` so that the same lemma works for `ℝ` and `ℝⁿ`; * generalize `real.image_Icc` etc to a conditionally complete linear order (e.g., now it works for `nnreal`, `ennreal`, `ereal`), move these lemmas to the `continuous_on` namespace. --- docs/undergrad.yaml | 2 +- src/analysis/box_integral/basic.lean | 2 +- src/analysis/box_integral/box/basic.lean | 2 +- .../box_integral/divergence_theorem.lean | 2 +- .../box_integral/partition/measure.lean | 2 +- src/data/set/intervals/basic.lean | 26 ++++ .../integral/interval_integral.lean | 14 +- src/topology/algebra/ordered/compact.lean | 141 +++++++++++++----- .../algebra/ordered/intermediate_value.lean | 14 ++ src/topology/instances/real.lean | 29 ---- 10 files changed, 156 insertions(+), 78 deletions(-) diff --git a/docs/undergrad.yaml b/docs/undergrad.yaml index a796dc26b9b89..6f045be960f17 100644 --- a/docs/undergrad.yaml +++ b/docs/undergrad.yaml @@ -307,7 +307,7 @@ Single Variable Real Analysis: continuity: 'continuous' limits: 'filter.tendsto' intermediate value theorem: 'intermediate_value_Icc' - image of a segment: 'real.image_Icc' + image of a segment: 'continuous_on.image_Icc' continuity of monotone functions: 'order_iso.continuous' continuity of inverse functions: 'order_iso.to_homeomorph' Differentiability: diff --git a/src/analysis/box_integral/basic.lean b/src/analysis/box_integral/basic.lean index 2e4f45315bf32..b2017495c3171 100644 --- a/src/analysis/box_integral/basic.lean +++ b/src/analysis/box_integral/basic.lean @@ -643,7 +643,7 @@ lemma integrable_of_continuous_on [complete_space E] {I : box ι} {f : ℝⁿ (hc : continuous_on f I.Icc) (μ : measure ℝⁿ) [is_locally_finite_measure μ] : integrable.{u v v} I l f μ.to_box_additive.to_smul := begin - have huc := (is_compact_pi_Icc I.lower I.upper).uniform_continuous_on_of_continuous hc, + have huc := I.is_compact_Icc.uniform_continuous_on_of_continuous hc, rw metric.uniform_continuous_on_iff_le at huc, refine integrable_iff_cauchy_basis.2 (λ ε ε0, _), rcases exists_pos_mul_lt ε0 (μ.to_box_additive I) with ⟨ε', ε0', hε⟩, diff --git a/src/analysis/box_integral/box/basic.lean b/src/analysis/box_integral/box/basic.lean index 7f20329839152..389e578cd9708 100644 --- a/src/analysis/box_integral/box/basic.lean +++ b/src/analysis/box_integral/box/basic.lean @@ -149,7 +149,7 @@ lemma Icc_def : I.Icc = Icc I.lower I.upper := rfl @[simp] lemma upper_mem_Icc (I : box ι) : I.upper ∈ I.Icc := right_mem_Icc.2 I.lower_le_upper @[simp] lemma lower_mem_Icc (I : box ι) : I.lower ∈ I.Icc := left_mem_Icc.2 I.lower_le_upper -protected lemma is_compact_Icc : is_compact I.Icc := is_compact_pi_Icc I.lower I.upper +protected lemma is_compact_Icc (I : box ι) : is_compact I.Icc := is_compact_Icc lemma Icc_eq_pi : I.Icc = pi univ (λ i, Icc (I.lower i) (I.upper i)) := (pi_univ_Icc _ _).symm diff --git a/src/analysis/box_integral/divergence_theorem.lean b/src/analysis/box_integral/divergence_theorem.lean index 8946c690b168f..57c87751d20a0 100644 --- a/src/analysis/box_integral/divergence_theorem.lean +++ b/src/analysis/box_integral/divergence_theorem.lean @@ -97,7 +97,7 @@ begin { intros y hy, refine (hε y hy).trans (mul_le_mul_of_nonneg_left _ h0.le), rw ← dist_eq_norm, - exact dist_le_diam_of_mem (is_compact_pi_Icc I.lower I.upper).bounded hy hxI }, + exact dist_le_diam_of_mem I.is_compact_Icc.bounded hy hxI }, rw [two_mul, add_mul], exact norm_sub_le_of_le (hε _ (this _ Hl)) (hε _ (this _ Hu)) } }, calc ∥(∏ j, (I.upper j - I.lower j)) • f' (pi.single i 1) - diff --git a/src/analysis/box_integral/partition/measure.lean b/src/analysis/box_integral/partition/measure.lean index 3d538050cce30..eaa177011ee6b 100644 --- a/src/analysis/box_integral/partition/measure.lean +++ b/src/analysis/box_integral/partition/measure.lean @@ -47,7 +47,7 @@ end lemma measurable_set_Icc [fintype ι] (I : box ι) : measurable_set I.Icc := measurable_set_Icc lemma measure_Icc_lt_top (μ : measure (ι → ℝ)) [is_locally_finite_measure μ] : μ I.Icc < ∞ := -show μ (Icc I.lower I.upper) < ∞, from (is_compact_pi_Icc I.lower I.upper).measure_lt_top +show μ (Icc I.lower I.upper) < ∞, from I.is_compact_Icc.measure_lt_top lemma measure_coe_lt_top (μ : measure (ι → ℝ)) [is_locally_finite_measure μ] : μ I < ∞ := (measure_mono $ coe_subset_Icc).trans_lt (I.measure_Icc_lt_top μ) diff --git a/src/data/set/intervals/basic.lean b/src/data/set/intervals/basic.lean index b312449d03881..d3e1098cd55cb 100644 --- a/src/data/set/intervals/basic.lean +++ b/src/data/set/intervals/basic.lean @@ -1212,6 +1212,32 @@ end end linear_order +/-! +### Closed intervals in `α × β` +-/ + +section prod + +variables {α β : Type*} [preorder α] [preorder β] + +@[simp] lemma Iic_prod_Iic (a : α) (b : β) : (Iic a).prod (Iic b) = Iic (a, b) := rfl + +@[simp] lemma Ici_prod_Ici (a : α) (b : β) : (Ici a).prod (Ici b) = Ici (a, b) := rfl + +lemma Ici_prod_eq (a : α × β) : Ici a = (Ici a.1).prod (Ici a.2) := rfl + +lemma Iic_prod_eq (a : α × β) : Iic a = (Iic a.1).prod (Iic a.2) := rfl + +@[simp] lemma Icc_prod_Icc (a₁ a₂ : α) (b₁ b₂ : β) : + (Icc a₁ a₂).prod (Icc b₁ b₂) = Icc (a₁, b₁) (a₂, b₂) := +by { ext ⟨x, y⟩, simp [and.assoc, and_comm, and.left_comm] } + +lemma Icc_prod_eq (a b : α × β) : + Icc a b = (Icc a.1 b.1).prod (Icc a.2 b.2) := +by simp + +end prod + /-! ### Lemmas about membership of arithmetic operations -/ section ordered_comm_group diff --git a/src/measure_theory/integral/interval_integral.lean b/src/measure_theory/integral/interval_integral.lean index 1ac1bea97ac9f..650d202b4d009 100644 --- a/src/measure_theory/integral/interval_integral.lean +++ b/src/measure_theory/integral/interval_integral.lean @@ -2276,19 +2276,19 @@ theorem integral_comp_smul_deriv'' {f f' : ℝ → ℝ} {g : ℝ → E} ∫ x in a..b, f' x • (g ∘ f) x= ∫ u in f a..f b, g u := begin have h_cont : continuous_on (λ u, ∫ t in f a..f u, g t) [a, b], - { rw [real.image_interval hf] at hg, + { rw [hf.image_interval] at hg, refine (continuous_on_primitive_interval' hg.interval_integrable _).comp hf _, - { rw [← real.image_interval hf], exact mem_image_of_mem f left_mem_interval }, - { rw [← image_subset_iff], exact (real.image_interval hf).subset } }, + { rw [← hf.image_interval], exact mem_image_of_mem f left_mem_interval }, + { rw [← image_subset_iff], exact hf.image_interval.subset } }, have h_der : ∀ x ∈ Ioo (min a b) (max a b), has_deriv_within_at (λ u, ∫ t in f a..f u, g t) (f' x • ((g ∘ f) x)) (Ioi x) x, { intros x hx, let I := [Inf (f '' [a, b]), Sup (f '' [a, b])], - have hI : f '' [a, b] = I := real.image_interval hf, + have hI : f '' [a, b] = I := hf.image_interval, have h2x : f x ∈ I, { rw [← hI], exact mem_image_of_mem f (Ioo_subset_Icc_self hx) }, have h2g : interval_integrable g volume (f a) (f x), { refine (hg.mono $ _).interval_integrable, - exact real.interval_subset_image_interval hf left_mem_interval (Ioo_subset_Icc_self hx) }, + exact hf.surj_on_interval left_mem_interval (Ioo_subset_Icc_self hx) }, rw [hI] at hg, have h3g : measurable_at_filter g (𝓝[I] f x) volume := hg.measurable_at_filter_nhds_within measurable_set_Icc (f x), @@ -2296,7 +2296,7 @@ begin have : has_deriv_within_at (λ u, ∫ x in f a..u, g x) (g (f x)) I (f x) := integral_has_deriv_within_at_right h2g h3g (hg (f x) h2x), refine (this.scomp x ((hff' x hx).Ioo_of_Ioi hx.2) _).Ioi_of_Ioo hx.2, - dsimp only [I], rw [← image_subset_iff, ← real.image_interval hf], + dsimp only [I], rw [← image_subset_iff, ← hf.image_interval], refine image_subset f (Ioo_subset_Icc_self.trans $ Icc_subset_Icc_left hx.1.le) }, have h_int : interval_integrable (λ (x : ℝ), f' x • (g ∘ f) x) volume a b := (hf'.smul (hg.comp hf $ subset_preimage_image f _)).interval_integrable, @@ -2339,7 +2339,7 @@ theorem integral_deriv_comp_smul_deriv' {f f' : ℝ → ℝ} {g g' : ℝ → E} begin rw [integral_comp_smul_deriv'' hf hff' hf' hg', integral_eq_sub_of_has_deriv_right hg hgg' (hg'.mono _).interval_integrable], - exact real.interval_subset_image_interval hf left_mem_interval right_mem_interval, + exact intermediate_value_interval hf end theorem integral_deriv_comp_smul_deriv {f f' : ℝ → ℝ} {g g' : ℝ → E} diff --git a/src/topology/algebra/ordered/compact.lean b/src/topology/algebra/ordered/compact.lean index 4207dc430af61..7fc4733155690 100644 --- a/src/topology/algebra/ordered/compact.lean +++ b/src/topology/algebra/ordered/compact.lean @@ -13,6 +13,9 @@ order topology (or a product of such types) is compact. We also prove the extrem (`is_compact.exists_forall_le`, `is_compact.exists_forall_ge`): a continuous function on a compact set takes its minimum and maximum values. +We also prove that the image of a closed interval under a continuous map is a closed interval, see +`continuous_on.image_Icc`. + ## Tags compact, extreme value theorem @@ -20,17 +23,32 @@ compact, extreme value theorem open classical filter order_dual topological_space function set -variables {α β : Type*} - [conditionally_complete_linear_order α] [topological_space α] [order_topology α] - [conditionally_complete_linear_order β] [topological_space β] [order_topology β] - /-! ### Compactness of a closed interval + +In this section we define a typeclass `compact_Icc_space α` saying that all closed intervals in `α` +are compact. Then we provide an instance for a `conditionally_complete_linear_order` and prove that +the product (both `α × β` and an indexed product) of spaces with this property inherits the +property. + +We also prove some simple lemmas about spaces with this property. -/ +/-- This typeclass says that all closed intervals in `α` are compact. This is true for all +conditionally complete linear orders with order topology and products (finite or infinite) +of such spaces. -/ +class compact_Icc_space (α : Type*) [topological_space α] [preorder α] : Prop := +(is_compact_Icc : ∀ {a b : α}, is_compact (Icc a b)) + +export compact_Icc_space (is_compact_Icc) + /-- A closed interval in a conditionally complete linear order is compact. -/ -lemma is_compact_Icc {a b : α} : is_compact (Icc a b) := +@[priority 100] +instance conditionally_complete_linear_order.to_compact_Icc_space + (α : Type*) [conditionally_complete_linear_order α] [topological_space α] [order_topology α] : + compact_Icc_space α := begin + refine ⟨λ a b, _⟩, cases le_or_lt a b with hab hab, swap, { simp [hab] }, refine is_compact_iff_ultrafilter_le_nhds.2 (λ f hf, _), contrapose! hf, @@ -72,32 +90,51 @@ begin { exact ((hsc.1 ⟨hy, hay⟩).not_lt hxy.1).elim }, end -/-- An unordered closed interval in a conditionally complete linear order is compact. -/ -lemma is_compact_interval {a b : α} : is_compact (interval a b) := is_compact_Icc +instance {ι : Type*} {α : ι → Type*} [Π i, preorder (α i)] [Π i, topological_space (α i)] + [Π i, compact_Icc_space (α i)] : compact_Icc_space (Π i, α i) := +⟨λ a b, pi_univ_Icc a b ▸ is_compact_univ_pi $ λ i, is_compact_Icc⟩ -lemma is_compact_pi_Icc {ι : Type*} {α : ι → Type*} [Π i, conditionally_complete_linear_order (α i)] - [Π i, topological_space (α i)] [Π i, order_topology (α i)] (a b : Π i, α i) : - is_compact (Icc a b) := -pi_univ_Icc a b ▸ is_compact_univ_pi $ λ i, is_compact_Icc +instance pi.compact_Icc_space' {α β : Type*} [preorder β] [topological_space β] + [compact_Icc_space β] : compact_Icc_space (α → β) := +pi.compact_Icc_space -instance compact_space_Icc (a b : α) : compact_space (Icc a b) := -is_compact_iff_compact_space.mp is_compact_Icc +instance {α β : Type*} [preorder α] [topological_space α] [compact_Icc_space α] + [preorder β] [topological_space β] [compact_Icc_space β] : + compact_Icc_space (α × β) := +⟨λ a b, (Icc_prod_eq a b).symm ▸ is_compact_Icc.prod is_compact_Icc⟩ + +/-- An unordered closed interval in a conditionally complete linear order is compact. -/ +lemma is_compact_interval {α : Type*} [conditionally_complete_linear_order α] + [topological_space α] [order_topology α]{a b : α} : is_compact (interval a b) := +is_compact_Icc -instance compact_space_pi_Icc {ι : Type*} {α : ι → Type*} - [Π i, conditionally_complete_linear_order (α i)] [Π i, topological_space (α i)] - [Π i, order_topology (α i)] (a b : Π i, α i) : compact_space (Icc a b) := -is_compact_iff_compact_space.mp (is_compact_pi_Icc a b) +/-- A complete linear order is a compact space. +We do not register an instance for a `[compact_Icc_space α]` because this would only add instances +for products (indexed or not) of complete linear orders, and we have instances with higher priority +that cover these cases. -/ @[priority 100] -- See note [lower instance priority] instance compact_space_of_complete_linear_order {α : Type*} [complete_linear_order α] [topological_space α] [order_topology α] : compact_space α := ⟨by simp only [← Icc_bot_top, is_compact_Icc]⟩ +section + +variables {α : Type*} [preorder α] [topological_space α] [compact_Icc_space α] + +instance compact_space_Icc (a b : α) : compact_space (Icc a b) := +is_compact_iff_compact_space.mp is_compact_Icc + +end + /-! ### Min and max elements of a compact set -/ +variables {α β : Type*} [conditionally_complete_linear_order α] [topological_space α] + [order_topology α] [topological_space β] + lemma is_compact.Inf_mem {s : set α} (hs : is_compact s) (ne_s : s.nonempty) : Inf s ∈ s := hs.is_closed.cInf_mem ne_s hs.bdd_below @@ -138,16 +175,16 @@ lemma is_compact.exists_is_lub {s : set α} (hs : is_compact s) (ne_s : s.nonemp ∃ x ∈ s, is_lub s x := ⟨_, hs.Sup_mem ne_s, hs.is_lub_Sup ne_s⟩ -lemma is_compact.exists_Inf_image_eq {α : Type*} [topological_space α] - {s : set α} (hs : is_compact s) (ne_s : s.nonempty) {f : α → β} (hf : continuous_on f s) : +lemma is_compact.exists_Inf_image_eq {s : set β} (hs : is_compact s) (ne_s : s.nonempty) + {f : β → α} (hf : continuous_on f s) : ∃ x ∈ s, Inf (f '' s) = f x := let ⟨x, hxs, hx⟩ := (hs.image_of_continuous_on hf).Inf_mem (ne_s.image f) in ⟨x, hxs, hx.symm⟩ -lemma is_compact.exists_Sup_image_eq {α : Type*} [topological_space α]: - ∀ {s : set α}, is_compact s → s.nonempty → ∀ {f : α → β}, continuous_on f s → +lemma is_compact.exists_Sup_image_eq : + ∀ {s : set β}, is_compact s → s.nonempty → ∀ {f : β → α}, continuous_on f s → ∃ x ∈ s, Sup (f '' s) = f x := -@is_compact.exists_Inf_image_eq (order_dual β) _ _ _ _ _ +@is_compact.exists_Inf_image_eq (order_dual α) _ _ _ _ _ lemma eq_Icc_of_connected_compact {s : set α} (h₁ : is_connected s) (h₂ : is_compact s) : s = Icc (Inf s) (Sup s) := @@ -158,8 +195,8 @@ eq_Icc_cInf_cSup_of_connected_bdd_closed h₁ h₂.bdd_below h₂.bdd_above h₂ -/ /-- The **extreme value theorem**: a continuous function realizes its minimum on a compact set. -/ -lemma is_compact.exists_forall_le {α : Type*} [topological_space α] - {s : set α} (hs : is_compact s) (ne_s : s.nonempty) {f : α → β} (hf : continuous_on f s) : +lemma is_compact.exists_forall_le {s : set β} (hs : is_compact s) (ne_s : s.nonempty) + {f : β → α} (hf : continuous_on f s) : ∃x∈s, ∀y∈s, f x ≤ f y := begin rcases (hs.image_of_continuous_on hf).exists_is_least (ne_s.image f) @@ -168,22 +205,22 @@ begin end /-- The **extreme value theorem**: a continuous function realizes its maximum on a compact set. -/ -lemma is_compact.exists_forall_ge {α : Type*} [topological_space α]: - ∀ {s : set α}, is_compact s → s.nonempty → ∀ {f : α → β}, continuous_on f s → +lemma is_compact.exists_forall_ge : + ∀ {s : set β}, is_compact s → s.nonempty → ∀ {f : β → α}, continuous_on f s → ∃x∈s, ∀y∈s, f y ≤ f x := -@is_compact.exists_forall_le (order_dual β) _ _ _ _ _ +@is_compact.exists_forall_le (order_dual α) _ _ _ _ _ /-- The **extreme value theorem**: if a continuous function `f` tends to infinity away from compact sets, then it has a global minimum. -/ -lemma continuous.exists_forall_le {α : Type*} [topological_space α] [nonempty α] {f : α → β} - (hf : continuous f) (hlim : tendsto f (cocompact α) at_top) : +lemma continuous.exists_forall_le [nonempty β] {f : β → α} + (hf : continuous f) (hlim : tendsto f (cocompact β) at_top) : ∃ x, ∀ y, f x ≤ f y := begin - inhabit α, - obtain ⟨s : set α, hsc : is_compact s, hsf : ∀ x ∉ s, f (default α) ≤ f x⟩ := - (has_basis_cocompact.tendsto_iff at_top_basis).1 hlim (f $ default α) trivial, - obtain ⟨x, -, hx⟩ := - (hsc.insert (default α)).exists_forall_le (nonempty_insert _ _) hf.continuous_on, + inhabit β, + obtain ⟨s : set β, hsc : is_compact s, hsf : ∀ x ∉ s, f (default β) ≤ f x⟩ := + (has_basis_cocompact.tendsto_iff at_top_basis).1 hlim (f $ default β) trivial, + obtain ⟨x, -, hx⟩ : ∃ x ∈ insert (default β) s, ∀ y ∈ insert (default β) s, f x ≤ f y := + (hsc.insert (default β)).exists_forall_le (nonempty_insert _ _) hf.continuous_on, refine ⟨x, λ y, _⟩, by_cases hy : y ∈ s, exacts [hx y (or.inr hy), (hx _ (or.inl rfl)).trans (hsf y hy)] @@ -191,7 +228,37 @@ end /-- The **extreme value theorem**: if a continuous function `f` tends to negative infinity away from compact sets, then it has a global maximum. -/ -lemma continuous.exists_forall_ge {α : Type*} [topological_space α] [nonempty α] {f : α → β} - (hf : continuous f) (hlim : tendsto f (cocompact α) at_bot) : +lemma continuous.exists_forall_ge [nonempty β] {f : β → α} + (hf : continuous f) (hlim : tendsto f (cocompact β) at_bot) : ∃ x, ∀ y, f y ≤ f x := -@continuous.exists_forall_le (order_dual β) _ _ _ _ _ _ _ hf hlim +@continuous.exists_forall_le (order_dual α) _ _ _ _ _ _ _ hf hlim + +/-! +### Image of a closed interval +-/ + +variables [densely_ordered α] [conditionally_complete_linear_order β] [order_topology β] + {f : α → β} {a b x y : α} + +open_locale interval + +lemma continuous_on.image_Icc (hab : a ≤ b) (h : continuous_on f $ Icc a b) : + f '' Icc a b = Icc (Inf $ f '' Icc a b) (Sup $ f '' Icc a b) := +eq_Icc_of_connected_compact ⟨(nonempty_Icc.2 hab).image f, is_preconnected_Icc.image f h⟩ + (is_compact_Icc.image_of_continuous_on h) + +lemma continuous_on.image_interval_eq_Icc (h : continuous_on f $ [a, b]) : + f '' [a, b] = Icc (Inf (f '' [a, b])) (Sup (f '' [a, b])) := +begin + cases le_total a b with h2 h2, + { simp_rw [interval_of_le h2] at h ⊢, exact h.image_Icc h2 }, + { simp_rw [interval_of_ge h2] at h ⊢, exact h.image_Icc h2 }, +end + +lemma continuous_on.image_interval (h : continuous_on f $ [a, b]) : + f '' [a, b] = [Inf (f '' [a, b]), Sup (f '' [a, b])] := +begin + refine h.image_interval_eq_Icc.trans (interval_of_le _).symm, + refine cInf_le_cSup _ _ (nonempty_interval.image _); rw h.image_interval_eq_Icc, + exacts [bdd_below_Icc, bdd_above_Icc] +end diff --git a/src/topology/algebra/ordered/intermediate_value.lean b/src/topology/algebra/ordered/intermediate_value.lean index 6e362fd050094..c56811284fbcd 100644 --- a/src/topology/algebra/ordered/intermediate_value.lean +++ b/src/topology/algebra/ordered/intermediate_value.lean @@ -520,6 +520,20 @@ or.elim (eq_or_lt_of_le hab) (λ he y h, absurd h.1 (not_lt_of_lt (he ▸ h.2))) _ _ ((hf.continuous_within_at ⟨hab, refl b⟩).mono Ioo_subset_Icc_self) ((hf.continuous_within_at ⟨refl a, hab⟩).mono Ioo_subset_Icc_self)) +/-- **Intermediate value theorem**: if `f` is continuous on an order-connected set `s` and `a`, +`b` are two points of this set, then `f` sends `s` to a superset of `Icc (f x) (f y)`. -/ +lemma continuous_on.surj_on_Icc {s : set α} [hs : ord_connected s] {f : α → δ} + (hf : continuous_on f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) : + surj_on f s (Icc (f a) (f b)) := +hs.is_preconnected.intermediate_value ha hb hf + +/-- **Intermediate value theorem**: if `f` is continuous on an order-connected set `s` and `a`, +`b` are two points of this set, then `f` sends `s` to a superset of `[f x, f y]`. -/ +lemma continuous_on.surj_on_interval {s : set α} [hs : ord_connected s] {f : α → δ} + (hf : continuous_on f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) : + surj_on f s (interval (f a) (f b)) := +by cases le_total (f a) (f b) with hab hab; simp [hf.surj_on_Icc, *] + /-- A continuous function which tendsto `at_top` `at_top` and to `at_bot` `at_bot` is surjective. -/ lemma continuous.surjective {f : α → δ} (hf : continuous f) (h_top : tendsto f at_top at_top) (h_bot : tendsto f at_bot at_bot) : diff --git a/src/topology/instances/real.lean b/src/topology/instances/real.lean index 6eadf18d66895..ef0db9e409685 100644 --- a/src/topology/instances/real.lean +++ b/src/topology/instances/real.lean @@ -308,35 +308,6 @@ lemma real.subset_Icc_Inf_Sup_of_bounded {s : set ℝ} (h : bounded s) : subset_Icc_cInf_cSup (real.bounded_iff_bdd_below_bdd_above.1 h).1 (real.bounded_iff_bdd_below_bdd_above.1 h).2 -lemma real.image_Icc {f : ℝ → ℝ} {a b : ℝ} (hab : a ≤ b) (h : continuous_on f $ Icc a b) : - f '' Icc a b = Icc (Inf $ f '' Icc a b) (Sup $ f '' Icc a b) := -eq_Icc_of_connected_compact ⟨(nonempty_Icc.2 hab).image f, is_preconnected_Icc.image f h⟩ - (is_compact_Icc.image_of_continuous_on h) - -lemma real.image_interval_eq_Icc {f : ℝ → ℝ} {a b : ℝ} (h : continuous_on f $ [a, b]) : - f '' [a, b] = Icc (Inf (f '' [a, b])) (Sup (f '' [a, b])) := -begin - cases le_total a b with h2 h2, - { simp_rw [interval_of_le h2] at h ⊢, exact real.image_Icc h2 h }, - { simp_rw [interval_of_ge h2] at h ⊢, exact real.image_Icc h2 h }, -end - -lemma real.image_interval {f : ℝ → ℝ} {a b : ℝ} (h : continuous_on f $ [a, b]) : - f '' [a, b] = [Inf (f '' [a, b]), Sup (f '' [a, b])] := -begin - refine (real.image_interval_eq_Icc h).trans (interval_of_le _).symm, - rw [real.image_interval_eq_Icc h], - exact real.Inf_le_Sup _ bdd_below_Icc bdd_above_Icc -end - -lemma real.interval_subset_image_interval {f : ℝ → ℝ} {a b x y : ℝ} - (h : continuous_on f [a, b]) (hx : x ∈ [a, b]) (hy : y ∈ [a, b]) : - [f x, f y] ⊆ f '' [a, b] := -begin - rw [real.image_interval h, interval_subset_interval_iff_mem, ← real.image_interval h], - exact ⟨mem_image_of_mem f hx, mem_image_of_mem f hy⟩ -end - end section periodic