refactor(topology/algebra/ordered): prove IVT for a connected set (#1806

)

* refactor(topology/algebra/ordered): prove IVT for a connected set

Also prove that intervals are connected, and deduce the classical IVT
from this.

* Rewrite the proof, move `min_le_max` to the root namespace

* Adjust `analysis/complex/exponential`

* Add comments/`obtain`

* Add some docs

* Add more docs

* Move some proofs to a section with weaker running assumptions

* Remove empty lines, fix a docstring

* +1 docstring

src/algebra/order.lean

@@ -175,9 +175,6 @@ lemma le_iff_le_iff_lt_iff_lt {β} [decidable_linear_order α] [decidable_linear
   {a b : α} {c d : β} : (a ≤ b ↔ c ≤ d) ↔ (b < a ↔ d < c) :=
 ⟨lt_iff_lt_of_le_iff_le, λ H, not_lt.symm.trans $ iff.trans (not_congr H) $ not_lt⟩
 
-lemma min_le_max [decidable_linear_order α] (a b : α) : min a b ≤ max a b :=
-le_trans (min_le_left a b) (le_max_left a b)
-
 end decidable
 
 namespace ordering

src/algebra/order_functions.lean

@@ -85,6 +85,7 @@ lemma max_min_distrib_left : max a (min b c) = min (max a b) (max a c) := sup_in
 lemma max_min_distrib_right : max (min a b) c = min (max a c) (max b c) := sup_inf_right
 lemma min_max_distrib_left : min a (max b c) = max (min a b) (min a c) := inf_sup_left
 lemma min_max_distrib_right : min (max a b) c = max (min a c) (min b c) := inf_sup_right
+lemma min_le_max : min a b ≤ max a b := le_trans (min_le_left a b) (le_max_left a b)
 
 instance max_idem : is_idempotent α max := by apply_instance -- short-circuit type class inference
 instance min_idem : is_idempotent α min := by apply_instance -- short-circuit type class inference

src/analysis/complex/exponential.lean

@@ -242,17 +242,14 @@ lemma differentiable_cosh : differentiable ℝ cosh :=
 lemma continuous_cosh : continuous cosh :=
 differentiable_cosh.continuous
 
-private lemma exists_exp_eq_of_one_le {x : ℝ} (hx : 1 ≤ x) : ∃ y, exp y = x :=
-let ⟨y, hy⟩ := @intermediate_value real.exp 0 (x - 1) x
-  (λ _ _ _, continuous_iff_continuous_at.1 continuous_exp _) (by simpa)
-  (by simpa using add_one_le_exp_of_nonneg (sub_nonneg.2 hx)) (sub_nonneg.2 hx) in
-⟨y, hy.2.2⟩
-
 lemma exists_exp_eq_of_pos {x : ℝ} (hx : 0 < x) : ∃ y, exp y = x :=
+have ∀ {z:ℝ}, 1 ≤ z → z ∈ set.range exp,
+  from λ z hz, intermediate_value_univ 0 (z - 1) continuous_exp
+    ⟨by simpa, by simpa using add_one_le_exp_of_nonneg (sub_nonneg.2 hz)⟩,
 match le_total x 1 with
-| (or.inl hx1) := let ⟨y, hy⟩ := exists_exp_eq_of_one_le (one_le_inv hx hx1) in
+| (or.inl hx1) := let ⟨y, hy⟩ := this (one_le_inv hx hx1) in
   ⟨-y, by rw [exp_neg, hy, inv_inv']⟩
-| (or.inr hx1) := exists_exp_eq_of_one_le hx1
+| (or.inr hx1) := this hx1
 end
 
 /-- The real logarithm function, equal to `0` for `x ≤ 0` and to the inverse of the exponential
@@ -374,11 +371,9 @@ show continuous ((log ∘ @subtype.val ℝ (λr, 0 < r)) ∘ λa, ⟨f a, h a⟩
 
 end prove_log_is_continuous
 
-lemma exists_cos_eq_zero : ∃ x, 1 ≤ x ∧ x ≤ 2 ∧ cos x = 0 :=
-real.intermediate_value'
-  (λ x _ _, continuous_iff_continuous_at.1 continuous_cos _)
-  (le_of_lt cos_one_pos)
-  (le_of_lt cos_two_neg) (by norm_num)
+lemma exists_cos_eq_zero : 0 ∈ cos '' set.Icc (1:ℝ) 2 :=
+intermediate_value_Icc' (by norm_num) continuous_cos.continuous_on
+  ⟨le_of_lt cos_two_neg, le_of_lt cos_one_pos⟩
 
 /-- The number π = 3.14159265... Defined here using choice as twice a zero of cos in [1,2], from
 which one can derive all its properties. For explicit bounds on π, see `data.real.pi`. -/
@@ -388,15 +383,15 @@ localized "notation `π` := real.pi" in real
 
 @[simp] lemma cos_pi_div_two : cos (π / 2) = 0 :=
 by rw [pi, mul_div_cancel_left _ (@two_ne_zero' ℝ _ _ _)];
-  exact (classical.some_spec exists_cos_eq_zero).2.2
+  exact (classical.some_spec exists_cos_eq_zero).2
 
 lemma one_le_pi_div_two : (1 : ℝ) ≤ π / 2 :=
 by rw [pi, mul_div_cancel_left _ (@two_ne_zero' ℝ _ _ _)];
-  exact (classical.some_spec exists_cos_eq_zero).1
+  exact (classical.some_spec exists_cos_eq_zero).1.1
 
 lemma pi_div_two_le_two : π / 2 ≤ 2 :=
 by rw [pi, mul_div_cancel_left _ (@two_ne_zero' ℝ _ _ _)];
-  exact (classical.some_spec exists_cos_eq_zero).2.1
+  exact (classical.some_spec exists_cos_eq_zero).1.2
 
 lemma two_le_pi : (2 : ℝ) ≤ π :=
 (div_le_div_right (show (0 : ℝ) < 2, by norm_num)).1
@@ -666,11 +661,10 @@ begin
   linarith
 end
 
-lemma exists_sin_eq {x : ℝ} (hx₁ : -1 ≤ x) (hx₂ : x ≤ 1) : ∃ y, -(π / 2) ≤ y ∧ y ≤ π / 2 ∧ sin y = x :=
-@real.intermediate_value sin (-(π / 2)) (π / 2) x
-  (λ _ _ _, continuous_iff_continuous_at.1 continuous_sin _)
-  (by rwa [sin_neg, sin_pi_div_two]) (by rwa sin_pi_div_two)
+lemma exists_sin_eq : set.Icc (-1:ℝ) 1 ⊆  sin '' set.Icc (-(π / 2)) (π / 2) :=
+by convert intermediate_value_Icc
   (le_trans (neg_nonpos.2 (le_of_lt pi_div_two_pos)) (le_of_lt pi_div_two_pos))
+  continuous_sin.continuous_on; simp only [sin_neg, sin_pi_div_two]
 
 lemma sin_lt {x : ℝ} (h : 0 < x) : sin x < x :=
 begin
@@ -793,21 +787,21 @@ end angle
 /-- Inverse of the `sin` function, returns values in the range `-π / 2 ≤ arcsin x` and `arcsin x ≤ π / 2`.
   If the argument is not between `-1` and `1` it defaults to `0` -/
 noncomputable def arcsin (x : ℝ) : ℝ :=
-if hx : -1 ≤ x ∧ x ≤ 1 then classical.some (exists_sin_eq hx.1 hx.2) else 0
+if hx : -1 ≤ x ∧ x ≤ 1 then classical.some (exists_sin_eq hx) else 0
 
 lemma arcsin_le_pi_div_two (x : ℝ) : arcsin x ≤ π / 2 :=
 if hx : -1 ≤ x ∧ x ≤ 1
-then by rw [arcsin, dif_pos hx]; exact (classical.some_spec (exists_sin_eq hx.1 hx.2)).2.1
+then by rw [arcsin, dif_pos hx]; exact (classical.some_spec (exists_sin_eq hx)).1.2
 else by rw [arcsin, dif_neg hx]; exact le_of_lt pi_div_two_pos
 
 lemma neg_pi_div_two_le_arcsin (x : ℝ) : -(π / 2) ≤ arcsin x :=
 if hx : -1 ≤ x ∧ x ≤ 1
-then by rw [arcsin, dif_pos hx]; exact (classical.some_spec (exists_sin_eq hx.1 hx.2)).1
+then by rw [arcsin, dif_pos hx]; exact (classical.some_spec (exists_sin_eq hx)).1.1
 else by rw [arcsin, dif_neg hx]; exact neg_nonpos.2 (le_of_lt pi_div_two_pos)
 
 lemma sin_arcsin {x : ℝ} (hx₁ : -1 ≤ x) (hx₂ : x ≤ 1) : sin (arcsin x) = x :=
 by rw [arcsin, dif_pos (and.intro hx₁ hx₂)];
-  exact (classical.some_spec (exists_sin_eq hx₁ hx₂)).2.2
+  exact (classical.some_spec (exists_sin_eq ⟨hx₁, hx₂⟩)).2
 
 lemma arcsin_sin {x : ℝ} (hx₁ : -(π / 2) ≤ x) (hx₂ : x ≤ π / 2) : arcsin (sin x) = x :=
 sin_inj_of_le_of_le_pi_div_two (neg_pi_div_two_le_arcsin _) (arcsin_le_pi_div_two _) hx₁ hx₂

src/topology/algebra/ordered.lean

@@ -2,14 +2,30 @@
 Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
-
-Theory of ordered topology.
 -/
 import order.liminf_limsup
 import data.set.intervals
 import topology.algebra.group
 import topology.constructions
 
+/-! # Theory of ordered topology
+
+## Main definitions
+`ordered_topology` and `orderable_topology`
+
+TODO expand
+
+## Main statements
+
+This file contains the proofs of the following facts:
+
+* all intervals `I??` are connected,
+* Intermediate Value Theorem, both for connected sets and `Icc` intervals,
+* Extreme Value Theorem: a continuous function on a compact set takes its maximum value.
+
+TODO expand
+-/
+
 open classical set lattice filter topological_space
 open_locale topological_space classical
 
@@ -119,6 +135,29 @@ is_open_lt continuous_const continuous_id
 lemma is_open_Ioo {a b : α} : is_open (Ioo a b) :=
 is_open_inter is_open_Ioi is_open_Iio
 
+lemma is_connected.forall_Icc_subset {s : set α} (hs : is_connected s)
+  {a b : α} (ha : a ∈ s) (hb : b ∈ s) :
+  Icc a b ⊆ s :=
+begin
+  assume x hx,
+  obtain ⟨y, hy, hy'⟩ : (s ∩ ((Iic x) ∩ (Ici x))).nonempty,
+    from is_connected_closed_iff.1 hs (Iic x) (Ici x) is_closed_Iic is_closed_Ici
+      (λ y _, le_total y x) ⟨a, ha, hx.1⟩ ⟨b, hb, hx.2⟩,
+  exact le_antisymm hy'.1 hy'.2 ▸ hy
+end
+
+/-- Intermediate Value Theorem for continuous functions on connected sets. -/
+lemma is_connected.intermediate_value {γ : Type*} [topological_space γ] {s : set γ}
+  (hs : is_connected s) {a b : γ} (ha : a ∈ s) (hb : b ∈ s) {f : γ → α} (hf : continuous_on f s) :
+  Icc (f a) (f b) ⊆ f '' s :=
+(hs.image f hf).forall_Icc_subset (mem_image_of_mem f ha) (mem_image_of_mem f hb)
+
+/-- Intermediate Value Theorem for continuous functions on connected spaces. -/
+lemma intermediate_value_univ {γ : Type*} [topological_space γ] [H : connected_space γ]
+  (a b : γ) {f : γ → α} (hf : continuous f) :
+  Icc (f a) (f b) ⊆ range f :=
+@image_univ _ _ f ▸ H.is_connected_univ.intermediate_value trivial trivial hf.continuous_on
+
 end linear_order
 
 section decidable_linear_order
@@ -995,6 +1034,82 @@ lemma cinfi_of_cinfi_of_monotone_of_continuous {f : α → β} {g : γ → α}
 by rw [infi, cInf_of_cInf_of_monotone_of_continuous Mf Cf
   (λ h, range_eq_empty.1 h ‹_›) H, ← range_comp]; refl
 
+section densely_ordered
+
+variables [densely_ordered α] {a b : α}
+
+lemma is_connected_Icc : is_connected (Icc a b) :=
+is_connected_closed_iff.2
+begin
+  rintros s t hs ht hab ⟨x, hx⟩ ⟨y, hy⟩,
+  wlog hxy : x ≤ y := le_total x y using [x y s t, y x t s],
+  -- `c = Sup (Icc x y ∩ s)` belongs to `Icc a b`, `s`, and `t`.
+  -- First two statements follow from general properties of `cSup`
+  let S := Icc x y ∩ s,
+  have xS : x ∈ S, from ⟨left_mem_Icc.2 hxy, hx.2⟩,
+  have Sne : S ≠ ∅, from ne_empty_iff_nonempty.2 ⟨x, xS⟩,
+  have Sbd : bdd_above S, from ⟨y, λ z hz, hz.1.2⟩,
+  let c := Sup S,
+  have c_mem : c ∈ S, from cSup_mem_of_is_closed Sne (is_closed_inter is_closed_Icc hs) Sbd,
+  have xyab : Icc x y ⊆ Icc a b := Icc_subset_Icc hx.1.1 hy.1.2,
+  have Sab : S ⊆ Icc a b := subset.trans (inter_subset_left _ _) xyab,
+  refine ⟨c, Sab c_mem, c_mem.2, _⟩,
+  -- Now we need to prove `c ∈ t`; we deduce it from `Ioc c y ⊆ (s ∪ t) \ s ⊆ t`
+  cases eq_or_lt_of_le c_mem.1.2 with hcy hcy, { exact hcy.symm ▸ hy.2 },
+  suffices : Icc c y ⊆ t, from this (left_mem_Icc.2 (le_of_lt hcy)),
+  rw [← closure_Ioc hcy, closure_subset_iff_subset_of_is_closed ht],
+  intros z hz,
+  have z_mem : z ∈ Icc x y, from Icc_subset_Icc_left c_mem.1.1 (Ioc_subset_Icc_self hz),
+  suffices : z ∈ t \ s, from and.left this,
+  rw [← union_diff_left],
+  exact ⟨hab $ xyab z_mem, λ zs, not_lt_of_le (le_cSup Sbd ⟨z_mem, zs⟩) hz.1⟩
+end
+
+lemma is_connected_iff_forall_Icc_subset {s : set α} :
+  is_connected s ↔ ∀ x y ∈ s, x ≤ y → Icc x y ⊆ s :=
+⟨λ h x y hx hy hxy, h.forall_Icc_subset hx hy, λ h, is_connected_of_forall_pair $ λ x y hx hy,
+  ⟨Icc (min x y) (max x y), h (min x y) (max x y)
+    ((min_choice x y).elim (λ h', by rwa h') (λ h', by rwa h'))
+    ((max_choice x y).elim (λ h', by rwa h') (λ h', by rwa h')) min_le_max,
+    ⟨min_le_left x y, le_max_left x y⟩, ⟨min_le_right x y, le_max_right x y⟩, is_connected_Icc⟩⟩
+
+lemma is_connected_Ici : is_connected (Ici a) :=
+is_connected_iff_forall_Icc_subset.2 $ λ x y hx hy hxy, (Icc_subset_Ici_iff hxy).2 hx
+
+lemma is_connected_Iic : is_connected (Iic a) :=
+is_connected_iff_forall_Icc_subset.2 $ λ x y hx hy hxy, (Icc_subset_Iic_iff hxy).2 hy
+
+lemma is_connected_Iio : is_connected (Iio a) :=
+is_connected_iff_forall_Icc_subset.2 $ λ x y hx hy hxy, (Icc_subset_Iio_iff hxy).2 hy
+
+lemma is_connected_Ioi : is_connected (Ioi a) :=
+is_connected_iff_forall_Icc_subset.2 $ λ x y hx hy hxy, (Icc_subset_Ioi_iff hxy).2 hx
+
+lemma is_connected_Ioo : is_connected (Ioo a b) :=
+is_connected_iff_forall_Icc_subset.2 $ λ x y hx hy hxy, (Icc_subset_Ioo_iff hxy).2 ⟨hx.1, hy.2⟩
+
+lemma is_connected_Ioc : is_connected (Ioc a b) :=
+is_connected_iff_forall_Icc_subset.2 $ λ x y hx hy hxy, (Icc_subset_Ioc_iff hxy).2 ⟨hx.1, hy.2⟩
+
+lemma is_connected_Ico : is_connected (Ico a b) :=
+is_connected_iff_forall_Icc_subset.2 $ λ x y hx hy hxy, (Icc_subset_Ico_iff hxy).2 ⟨hx.1, hy.2⟩
+
+@[priority 100]
+instance ordered_connected_space : connected_space α :=
+⟨is_connected_iff_forall_Icc_subset.2 $ λ x y hx hy hxy, subset_univ _⟩
+
+/--Intermediate Value Theorem for continuous functions on closed intervals, case `f a ≤ t ≤ f b`.-/
+lemma intermediate_value_Icc {a b : α} (hab : a ≤ b) {f : α → β} (hf : continuous_on f (Icc a b)) :
+  Icc (f a) (f b) ⊆ f '' (Icc a b) :=
+is_connected_Icc.intermediate_value (left_mem_Icc.2 hab) (right_mem_Icc.2 hab) hf
+
+/--Intermediate Value Theorem for continuous functions on closed intervals, case `f a ≥ t ≥ f b`.-/
+lemma intermediate_value_Icc' {a b : α} (hab : a ≤ b) {f : α → β} (hf : continuous_on f (Icc a b)) :
+  Icc (f b) (f a) ⊆ f '' (Icc a b) :=
+is_connected_Icc.intermediate_value (right_mem_Icc.2 hab) (left_mem_Icc.2 hab) hf
+
+end densely_ordered
+
 /-- The extreme value theorem: a continuous function realizes its minimum on a compact set -/
 lemma exists_forall_le_of_compact_of_continuous {α : Type u} [topological_space α]
   (f : α → β) (hf : continuous f) (s : set α) (hs : compact s) (ne_s : s ≠ ∅) :

src/topology/instances/real.lean

@@ -347,60 +347,6 @@ compact_of_totally_bounded_is_closed
 instance : proper_space ℝ :=
 { compact_ball := λx r, by rw closed_ball_Icc; apply compact_Icc }
 
-open real
-
-lemma real.intermediate_value {f : ℝ → ℝ} {a b t : ℝ}
-  (hf : ∀ x, a ≤ x → x ≤ b → tendsto f (𝓝 x) (𝓝 (f x)))
-  (ha : f a ≤ t) (hb : t ≤ f b) (hab : a ≤ b) : ∃ x : ℝ, a ≤ x ∧ x ≤ b ∧ f x = t :=
-let x := real.Sup {x | f x ≤ t ∧ a ≤ x ∧ x ≤ b} in
-have hx₁ : ∃ y, ∀ g ∈ {x | f x ≤ t ∧ a ≤ x ∧ x ≤ b}, g ≤ y := ⟨b, λ _ h, h.2.2⟩,
-have hx₂ : ∃ y, y ∈ {x | f x ≤ t ∧ a ≤ x ∧ x ≤ b} := ⟨a, ha, le_refl _, hab⟩,
-have hax : a ≤ x, from le_Sup _ hx₁ ⟨ha, le_refl _, hab⟩,
-have hxb : x ≤ b, from (Sup_le _ hx₂ hx₁).2 (λ _ h, h.2.2),
-⟨x, hax, hxb,
-  eq_of_forall_dist_le $ λ ε ε0,
-    let ⟨δ, hδ0, hδ⟩ := metric.tendsto_nhds_nhds.1 (hf _ hax hxb) ε ε0 in
-    (le_total t (f x)).elim
-      (λ h, le_of_not_gt $ λ hfε, begin
-        rw [dist_eq, abs_of_nonneg (sub_nonneg.2 h)] at hfε,
-        refine mt (Sup_le {x | f x ≤ t ∧ a ≤ x ∧ x ≤ b} hx₂ hx₁).2
-          (not_le_of_gt (sub_lt_self x (half_pos hδ0)))
-          (λ g hg, le_of_not_gt
-            (λ hgδ, not_lt_of_ge hg.1
-              (lt_trans (lt_sub.1 hfε) (sub_lt_of_sub_lt
-                (lt_of_le_of_lt (le_abs_self _) _))))),
-        rw abs_sub,
-        exact hδ (abs_sub_lt_iff.2 ⟨lt_of_le_of_lt (sub_nonpos.2 (le_Sup _ hx₁ hg)) hδ0,
-          by simp only [x] at *; linarith⟩)
-        end)
-      (λ h, le_of_not_gt $ λ hfε, begin
-        rw [dist_eq, abs_of_nonpos (sub_nonpos.2 h)] at hfε,
-        exact mt (le_Sup {x | f x ≤ t ∧ a ≤ x ∧ x ≤ b})
-          (λ h : ∀ k, k ∈ {x | f x ≤ t ∧ a ≤ x ∧ x ≤ b} → k ≤ x,
-            not_le_of_gt ((lt_add_iff_pos_left x).2 (half_pos hδ0))
-              (h _ ⟨le_trans (le_sub_iff_add_le.2 (le_trans (le_abs_self _)
-                    (le_of_lt (hδ $ by rw [dist_eq, add_sub_cancel, abs_of_nonneg (le_of_lt (half_pos hδ0))];
-                      exact half_lt_self hδ0))))
-                  (by linarith),
-                le_trans hax (le_of_lt ((lt_add_iff_pos_left _).2 (half_pos hδ0))),
-                le_of_not_gt (λ hδy, not_lt_of_ge hb (lt_of_le_of_lt
-                  (show f b ≤ f b - f x - ε + t, by linarith)
-                  (add_lt_of_neg_of_le
-                    (sub_neg_of_lt (lt_of_le_of_lt (le_abs_self _)
-                      (@hδ b (abs_sub_lt_iff.2 ⟨by simp only [x] at *; linarith,
-                        by linarith⟩))))
-                    (le_refl _))))⟩))
-          hx₁
-        end)⟩
-
-lemma real.intermediate_value' {f : ℝ → ℝ} {a b t : ℝ}
-  (hf : ∀ x, a ≤ x → x ≤ b → tendsto f (𝓝 x) (𝓝 (f x)))
-  (ha : t ≤ f a) (hb : f b ≤ t) (hab : a ≤ b) : ∃ x : ℝ, a ≤ x ∧ x ≤ b ∧ f x = t :=
-let ⟨x, hx₁, hx₂, hx₃⟩ := @real.intermediate_value
-  (λ x, - f x) a b (-t) (λ x hax hxb, (hf x hax hxb).neg)
-  (neg_le_neg ha) (neg_le_neg hb) hab in
-⟨x, hx₁, hx₂, neg_inj hx₃⟩
-
 lemma real.bounded_iff_bdd_below_bdd_above {s : set ℝ} : bounded s ↔ bdd_below s ∧ bdd_above s :=
 ⟨begin
   assume bdd,