[Merged by Bors] - feat(continuous_function/compact): lemmas characterising norm and dist

src/topology/continuous_function/bounded.lean

@@ -123,7 +123,7 @@ le_cInf dist_set_exists (λ C, and.left)
 lemma dist_le (C0 : (0 : ℝ) ≤ C) : dist f g ≤ C ↔ ∀x:α, dist (f x) (g x) ≤ C :=
 ⟨λ h x, le_trans (dist_coe_le_dist x) h, λ H, cInf_le ⟨0, λ C, and.left⟩ ⟨C0, H⟩⟩
 
-lemma dist_le_of_nonempty [nonempty α] :
+lemma dist_le_iff_of_nonempty [nonempty α] :
   dist f g ≤ C ↔ ∀ x, dist (f x) (g x) ≤ C :=
 ⟨λ h x, le_trans (dist_coe_le_dist x) h,
  λ w, (dist_le (le_trans dist_nonneg (w (nonempty.some ‹_›)))).mpr w⟩
@@ -134,7 +134,7 @@ begin
   have c : continuous (λ x, dist (f x) (g x)), { continuity, },
   obtain ⟨x, -, le⟩ :=
     is_compact.exists_forall_ge compact_univ set.univ_nonempty (continuous.continuous_on c),
-  exact lt_of_le_of_lt (dist_le_of_nonempty.mpr (λ y, le y trivial)) (w x),
+  exact lt_of_le_of_lt (dist_le_iff_of_nonempty.mpr (λ y, le y trivial)) (w x),
 end
 
 lemma dist_lt_iff_of_compact [compact_space α] (C0 : (0 : ℝ) < C) :
@@ -467,7 +467,7 @@ lemma norm_le_of_nonempty [nonempty α]
   {f : α →ᵇ β} {M : ℝ} : ∥f∥ ≤ M ↔ ∀ x, ∥f x∥ ≤ M :=
 begin
   simp_rw [norm_def, ←dist_zero_right],
-  exact dist_le_of_nonempty,
+  exact dist_le_iff_of_nonempty,
 end
 
 lemma norm_lt_iff_of_compact [compact_space α]

src/topology/continuous_function/compact.lean

@@ -5,6 +5,7 @@ Authors: Scott Morrison
 -/
 import topology.continuous_function.bounded
 import analysis.normed_space.linear_isometry
+import topology.uniform_space.compact_separated
 import tactic.equiv_rw
 
 /-!
@@ -27,12 +28,12 @@ open_locale topological_space classical nnreal bounded_continuous_function
 
 open set filter metric
 
-variables (α : Type*) (β : Type*) [topological_space α] [compact_space α] [normed_group β]
-
 open bounded_continuous_function
 
 namespace continuous_map
 
+variables (α : Type*) (β : Type*) [topological_space α] [compact_space α] [normed_group β]
+
 /--
 When `α` is compact, the bounded continuous maps `α →ᵇ 𝕜` are
 equivalent to `C(α, 𝕜)`.
@@ -68,6 +69,36 @@ metric_space.induced
   (equiv_bounded_of_compact α β).injective
   (by apply_instance)
 
+section
+variables {α β} (f g : C(α, β)) {C : ℝ}
+
+/-- The distance between two functions is controlled by the supremum of the pointwise distances -/
+lemma dist_le (C0 : (0 : ℝ) ≤ C) : dist f g ≤ C ↔ ∀x:α, dist (f x) (g x) ≤ C :=
+@bounded_continuous_function.dist_le  _ _ _ _
+  ((equiv_bounded_of_compact α β) f) ((equiv_bounded_of_compact α β) g) _ C0
+
+lemma dist_le_iff_of_nonempty [nonempty α] :
+  dist f g ≤ C ↔ ∀ x, dist (f x) (g x) ≤ C :=
+@bounded_continuous_function.dist_le_iff_of_nonempty  _ _ _ _
+  ((equiv_bounded_of_compact α β) f) ((equiv_bounded_of_compact α β) g) _ _
+
+lemma dist_lt_of_nonempty [nonempty α]
+  (w : ∀x:α, dist (f x) (g x) < C) : dist f g < C :=
+@bounded_continuous_function.dist_lt_of_nonempty_compact  _ _ _ _
+  ((equiv_bounded_of_compact α β) f) ((equiv_bounded_of_compact α β) g) _ _ _ w
+
+lemma dist_lt_iff (C0 : (0 : ℝ) < C) :
+  dist f g < C ↔ ∀x:α, dist (f x) (g x) < C :=
+@bounded_continuous_function.dist_lt_iff_of_compact  _ _ _ _
+  ((equiv_bounded_of_compact α β) f) ((equiv_bounded_of_compact α β) g) _ _ C0
+
+lemma dist_lt_iff_of_nonempty [nonempty α] :
+  dist f g < C ↔ ∀x:α, dist (f x) (g x) < C :=
+@bounded_continuous_function.dist_lt_iff_of_nonempty_compact  _ _ _ _
+  ((equiv_bounded_of_compact α β) f) ((equiv_bounded_of_compact α β) g) _ _ _
+
+end
+
 variables (α β)
 
 /--
@@ -97,6 +128,35 @@ instance : normed_group C(α,β) :=
     exact ((add_equiv_bounded_of_compact α β).symm.map_sub _ _).symm,
   end, }
 
+section
+variables {α β} (f : C(α, β))
+-- The corresponding lemmas for `bounded_continuous_function` are stated with `{f}`,
+-- and so can not be used in dot notation.
+
+/-- Distance between the images of any two points is at most twice the norm of the function. -/
+lemma dist_le_two_norm (x y : α) : dist (f x) (f y) ≤ 2 * ∥f∥ :=
+((equiv_bounded_of_compact α β) f).dist_le_two_norm x y
+
+/-- The norm of a function is controlled by the supremum of the pointwise norms -/
+lemma norm_le {C : ℝ} (C0 : (0 : ℝ) ≤ C) : ∥f∥ ≤ C ↔ ∀x:α, ∥f x∥ ≤ C :=
+@bounded_continuous_function.norm_le _ _ _ _
+  ((equiv_bounded_of_compact α β) f) _ C0
+
+lemma norm_le_of_nonempty [nonempty α] {M : ℝ} : ∥f∥ ≤ M ↔ ∀ x, ∥f x∥ ≤ M :=
+@bounded_continuous_function.norm_le_of_nonempty _ _ _ _ _
+  ((equiv_bounded_of_compact α β) f) _
+
+lemma norm_lt_iff {M : ℝ} (M0 : 0 < M) : ∥f∥ < M ↔ ∀ x, ∥f x∥ < M :=
+@bounded_continuous_function.norm_lt_iff_of_compact _ _ _ _ _
+  ((equiv_bounded_of_compact α β) f) _ M0
+
+lemma norm_lt_iff_of_nonempty [nonempty α] {M : ℝ} :
+  ∥f∥ < M ↔ ∀ x, ∥f x∥ < M :=
+@bounded_continuous_function.norm_lt_iff_of_nonempty_compact _ _ _ _ _ _
+  ((equiv_bounded_of_compact α β) f) _
+
+end
+
 section
 variables {R : Type*} [normed_ring R]