chore(topology): generalize real.image_Icc etc (#9784)

* 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.

Author: urkud

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:

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ε⟩,

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
 

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) -

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 μ)

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

src/measure_theory/integral/interval_integral.lean

@@ -2276,27 +2276,27 @@ 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),
     haveI : fact (f x ∈ I) := ⟨h2x⟩,
     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}

src/topology/algebra/ordered/compact.lean

@@ -13,24 +13,42 @@ 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
 -/
 
 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,30 +205,60 @@ 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)]
 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

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) :

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