feat(topology): properties about intervals and paths (#9914)

* From the sphere eversion project
* Properties about paths, the interval, and `proj_Icc`

src/analysis/special_functions/trigonometric/inverse.lean

@@ -68,7 +68,7 @@ inj_on_arcsin.eq_iff ⟨hx₁, hx₂⟩ ⟨hy₁, hy₂⟩
 
 @[continuity]
 lemma continuous_arcsin : continuous arcsin :=
-continuous_subtype_coe.comp sin_order_iso.symm.continuous.Icc_extend
+continuous_subtype_coe.comp sin_order_iso.symm.continuous.Icc_extend'
 
 lemma continuous_at_arcsin {x : ℝ} : continuous_at arcsin x :=
 continuous_arcsin.continuous_at

src/data/set/intervals/proj_Icc.lean

@@ -42,6 +42,21 @@ by simp [proj_Icc, hx, h]
 @[simp] lemma proj_Icc_right : proj_Icc a b h b = ⟨b, right_mem_Icc.2 h⟩ :=
 proj_Icc_of_right_le h le_rfl
 
+lemma proj_Icc_eq_left (h : a < b) : proj_Icc a b h.le x = ⟨a, left_mem_Icc.mpr h.le⟩ ↔ x ≤ a :=
+begin
+  refine ⟨λ h', _, proj_Icc_of_le_left _⟩,
+  simp_rw [subtype.ext_iff_val, proj_Icc, max_eq_left_iff, min_le_iff, h.not_le, false_or] at h',
+  exact h'
+end
+
+lemma proj_Icc_eq_right (h : a < b) : proj_Icc a b h.le x = ⟨b, right_mem_Icc.mpr h.le⟩ ↔ b ≤ x :=
+begin
+  refine ⟨λ h', _, proj_Icc_of_right_le _⟩,
+  simp_rw [subtype.ext_iff_val, proj_Icc] at h',
+  have := ((max_choice _ _).resolve_left (by simp [h.ne', h'])).symm.trans h',
+  exact min_eq_left_iff.mp this
+end
+
 lemma proj_Icc_of_mem (hx : x ∈ Icc a b) : proj_Icc a b h x = ⟨x, hx⟩ :=
 by simp [proj_Icc, hx.1, hx.2]
 

src/topology/algebra/ordered/proj_Icc.lean

@@ -13,10 +13,18 @@ In this file we prove that the projection `set.proj_Icc f a b h` is a quotient m
 to show that `Icc_extend h f` is continuous if and only if `f` is continuous.
 -/
 
-variables {α β : Type*} [topological_space α] [linear_order α] [order_topology α]
-  [topological_space β] {a b : α} {h : a ≤ b}
+open set filter
+open_locale filter topological_space
 
-open set
+variables {α β γ : Type*} [linear_order α] [topological_space γ] {a b c : α} {h : a ≤ b}
+
+lemma filter.tendsto.Icc_extend (f : γ → Icc a b → β) {z : γ} {l : filter α} {l' : filter β}
+  (hf : tendsto ↿f (𝓝 z ×ᶠ l.map (proj_Icc a b h)) l') :
+  tendsto ↿(Icc_extend h ∘ f) (𝓝 z ×ᶠ l) l' :=
+show tendsto (↿f ∘ prod.map id (proj_Icc a b h)) (𝓝 z ×ᶠ l) l', from
+hf.comp $ tendsto_id.prod_map tendsto_map
+
+variables [topological_space α] [order_topology α] [topological_space β]
 
 @[continuity]
 lemma continuous_proj_Icc : continuous (proj_Icc a b h) :=
@@ -31,7 +39,18 @@ quotient_map_iff.2 ⟨proj_Icc_surjective h, λ s,
   continuous (Icc_extend h f) ↔ continuous f :=
 quotient_map_proj_Icc.continuous_iff.symm
 
+/-- See Note [continuity lemma statement]. -/
+lemma continuous.Icc_extend {f : γ → Icc a b → β} {g : γ → α}
+  (hf : continuous ↿f) (hg : continuous g) : continuous (λ a, Icc_extend h (f a) (g a)) :=
+hf.comp $ continuous_id.prod_mk $ continuous_proj_Icc.comp hg
+
+/-- A useful special case of `continuous.Icc_extend`. -/
 @[continuity]
-lemma continuous.Icc_extend {f : Icc a b → β} (hf : continuous f) :
-  continuous (Icc_extend h f) :=
+lemma continuous.Icc_extend' {f : Icc a b → β} (hf : continuous f) : continuous (Icc_extend h f) :=
 hf.comp continuous_proj_Icc
+
+lemma continuous_at.Icc_extend {x : γ} (f : γ → Icc a b → β) {g : γ → α}
+  (hf : continuous_at ↿f (x, proj_Icc a b h (g x))) (hg : continuous_at g x) :
+  continuous_at (λ a, Icc_extend h (f a) (g a)) x :=
+show continuous_at (↿f ∘ λ x, (x, proj_Icc a b h (g x))) x, from
+continuous_at.comp hf $ continuous_at_id.prod $ continuous_proj_Icc.continuous_at.comp hg

src/topology/path_connected.lean

@@ -62,7 +62,7 @@ noncomputable theory
 open_locale classical topological_space filter unit_interval
 open filter set function unit_interval
 
-variables {X : Type*} [topological_space X] {x y z : X} {ι : Type*}
+variables {X Y : Type*} [topological_space X] [topological_space Y] {x y z : X} {ι : Type*}
 
 /-! ### Paths -/
 
@@ -74,8 +74,7 @@ structure path (x y : X) extends C(I, X) :=
 
 instance : has_coe_to_fun (path x y) (λ _, I → X) := ⟨λ p, p.to_fun⟩
 
-@[ext] protected lemma path.ext {X : Type*} [topological_space X] {x y : X} :
-  ∀ {γ₁ γ₂ : path x y}, (γ₁ : I → X) = γ₂ → γ₁ = γ₂
+@[ext] protected lemma path.ext : ∀ {γ₁ γ₂ : path x y}, (γ₁ : I → X) = γ₂ → γ₁ = γ₂
 | ⟨⟨x, h11⟩, h12, h13⟩ ⟨⟨.(x), h21⟩, h22, h23⟩ rfl := rfl
 
 namespace path
@@ -114,8 +113,7 @@ instance has_uncurry_path {X α : Type*} [topological_space X] {x y : α → X}
   source' := rfl,
   target' := rfl }
 
-@[simp] lemma refl_range {X : Type*} [topological_space X] {a : X} :
-  range (path.refl a) = {a} :=
+@[simp] lemma refl_range {a : X} : range (path.refl a) = {a} :=
 by simp [path.refl, has_coe_to_fun.coe, coe_fn]
 
 /-- The reverse of a path from `x` to `y`, as a path from `y` to `x` -/
@@ -128,12 +126,10 @@ by simp [path.refl, has_coe_to_fun.coe, coe_fn]
 @[simp] lemma symm_symm {γ : path x y} : γ.symm.symm = γ :=
 by { ext, simp }
 
-@[simp] lemma refl_symm {X : Type*} [topological_space X] {a : X} :
-  (path.refl a).symm = path.refl a :=
+@[simp] lemma refl_symm {a : X} : (path.refl a).symm = path.refl a :=
 by { ext, refl }
 
-@[simp] lemma symm_range {X : Type*} [topological_space X] {a b : X} (γ : path a b) :
-  range γ.symm = range γ :=
+@[simp] lemma symm_range {a b : X} (γ : path a b) : range γ.symm = range γ :=
 begin
   ext x,
   simp only [mem_range, path.symm, has_coe_to_fun.coe, coe_fn, unit_interval.symm, set_coe.exists,
@@ -145,9 +141,26 @@ end
 /-- A continuous map extending a path to `ℝ`, constant before `0` and after `1`. -/
 def extend : ℝ → X := Icc_extend zero_le_one γ
 
+/-- See Note [continuity lemma statement]. -/
+lemma _root_.continuous.path_extend {γ : Y → path x y} {f : Y → ℝ} (hγ : continuous ↿γ)
+  (hf : continuous f) : continuous (λ t, (γ t).extend (f t)) :=
+continuous.Icc_extend hγ hf
+
+/-- A useful special case of `continuous.path_extend`. -/
 @[continuity]
 lemma continuous_extend : continuous γ.extend :=
-γ.continuous.Icc_extend
+γ.continuous.Icc_extend'
+
+lemma _root_.filter.tendsto.path_extend {X Y : Type*} [topological_space X] [topological_space Y]
+  {l r : Y → X} {y : Y} {l₁ : filter ℝ} {l₂ : filter X} {γ : ∀ y, path (l y) (r y)}
+  (hγ : tendsto ↿γ (𝓝 y ×ᶠ l₁.map (proj_Icc 0 1 zero_le_one)) l₂) :
+  tendsto ↿(λ x, (γ x).extend) (𝓝 y ×ᶠ l₁) l₂ :=
+filter.tendsto.Icc_extend _ hγ
+
+lemma _root_.continuous_at.path_extend {g : Y → ℝ} {l r : Y → X} (γ : ∀ y, path (l y) (r y)) {y : Y}
+  (hγ : continuous_at ↿γ (y, proj_Icc 0 1 zero_le_one (g y)))
+  (hg : continuous_at g y) : continuous_at (λ i, (γ i).extend (g i)) y :=
+hγ.Icc_extend (λ x, γ x) hg
 
 @[simp] lemma extend_extends {X : Type*} [topological_space X] {a b : X}
   (γ : path a b) {t : ℝ} (ht : t ∈ (Icc 0 1 : set ℝ)) : γ.extend t = γ ⟨t, ht⟩ :=

src/topology/unit_interval.lean

@@ -5,14 +5,15 @@ Authors: Patrick Massot, Scott Morrison
 -/
 import topology.instances.real
 import topology.algebra.field
+import data.set.intervals.proj_Icc
 
 /-!
 # The unit interval, as a topological space
 
 Use `open_locale unit_interval` to turn on the notation `I := set.Icc (0 : ℝ) (1 : ℝ)`.
 
 We provide basic instances, as well as a custom tactic for discharging
-`0 ≤ x`, `0 ≤ 1 - x`, `x ≤ 1`, and `1 - x ≤ 1` when `x : I`.
+`0 ≤ ↑x`, `0 ≤ 1 - ↑x`, `↑x ≤ 1`, and `1 - ↑x ≤ 1` when `x : I`.
 
 -/
 
@@ -41,14 +42,41 @@ instance has_zero : has_zero I := ⟨⟨0, by split ; norm_num⟩⟩
 
 @[simp] lemma mk_zero (h : (0 : ℝ) ∈ Icc (0 : ℝ) 1) : (⟨0, h⟩ : I) = 0 := rfl
 
+@[simp, norm_cast] lemma coe_eq_zero {x : I} : (x : ℝ) = 0 ↔ x = 0 :=
+by { symmetry, exact subtype.ext_iff }
+
 instance has_one : has_one I := ⟨⟨1, by split ; norm_num⟩⟩
 
 @[simp, norm_cast] lemma coe_one : ((1 : I) : ℝ) = 1 := rfl
 
+lemma coe_ne_zero {x : I} : (x : ℝ) ≠ 0 ↔ x ≠ 0 :=
+not_iff_not.mpr coe_eq_zero
+
 @[simp] lemma mk_one (h : (1 : ℝ) ∈ Icc (0 : ℝ) 1) : (⟨1, h⟩ : I) = 1 := rfl
 
+@[simp, norm_cast] lemma coe_eq_one {x : I} : (x : ℝ) = 1 ↔ x = 1 :=
+by { symmetry, exact subtype.ext_iff }
+
+lemma coe_ne_one {x : I} : (x : ℝ) ≠ 1 ↔ x ≠ 1 :=
+not_iff_not.mpr coe_eq_one
+
 instance : nonempty I := ⟨0⟩
 
+lemma mul_mem (x y : I) : (x : ℝ) * y ∈ I :=
+⟨mul_nonneg x.2.1 y.2.1, (mul_le_mul x.2.2 y.2.2 y.2.1 zero_le_one).trans_eq $ one_mul 1⟩
+
+instance : has_mul I := ⟨λ x y, ⟨x * y, mul_mem x y⟩⟩
+
+@[simp, norm_cast] lemma coe_mul {x y : I} : ((x * y : I) : ℝ) = x * y := rfl
+
+-- todo: we could set up a `linear_ordered_comm_monoid_with_zero I` instance
+
+lemma mul_le_left {x y : I} : x * y ≤ x :=
+subtype.coe_le_coe.mp $ (mul_le_mul_of_nonneg_left y.2.2 x.2.1).trans_eq $ mul_one x
+
+lemma mul_le_right {x y : I} : x * y ≤ y :=
+subtype.coe_le_coe.mp $ (mul_le_mul_of_nonneg_right x.2.2 y.2.1).trans_eq $ one_mul y
+
 /-- Unit interval central symmetry. -/
 def symm : I → I := λ t, ⟨1 - t.val, mem_iff_one_sub_mem.mp t.property⟩
 
@@ -80,6 +108,11 @@ lemma one_minus_nonneg (x : I) : 0 ≤ 1 - (x : ℝ) := by simpa using x.2.2
 lemma le_one (x : I) : (x : ℝ) ≤ 1 := x.2.2
 lemma one_minus_le_one (x : I) : 1 - (x : ℝ) ≤ 1 := by simpa using x.2.1
 
+/-- like `unit_interval.nonneg`, but with the inequality in `I`. -/
+lemma nonneg' {t : I} : 0 ≤ t := t.2.1
+/-- like `unit_interval.le_one`, but with the inequality in `I`. -/
+lemma le_one' {t : I} : t ≤ 1 := t.2.2
+
 lemma mul_pos_mem_iff {a t : ℝ} (ha : 0 < a) : a * t ∈ I ↔ t ∈ set.Icc (0 : ℝ) (1/a) :=
 begin
   split; rintros ⟨h₁, h₂⟩; split,
@@ -94,9 +127,15 @@ by split; rintros ⟨h₁, h₂⟩; split; linarith
 
 end unit_interval
 
+@[simp] lemma proj_Icc_eq_zero {x : ℝ} : proj_Icc (0 : ℝ) 1 zero_le_one x = 0 ↔ x ≤ 0 :=
+proj_Icc_eq_left zero_lt_one
+
+@[simp] lemma proj_Icc_eq_one {x : ℝ} : proj_Icc (0 : ℝ) 1 zero_le_one x = 1 ↔ 1 ≤ x :=
+proj_Icc_eq_right zero_lt_one
+
 namespace tactic.interactive
 
-/-- A tactic that solves `0 ≤ x`, `0 ≤ 1 - x`, `x ≤ 1`, and `1 - x ≤ 1` for `x : I`. -/
+/-- A tactic that solves `0 ≤ ↑x`, `0 ≤ 1 - ↑x`, `↑x ≤ 1`, and `1 - ↑x ≤ 1` for `x : I`. -/
 meta def unit_interval : tactic unit :=
 `[apply unit_interval.nonneg] <|> `[apply unit_interval.one_minus_nonneg] <|>
 `[apply unit_interval.le_one] <|> `[apply unit_interval.one_minus_le_one]