complete sets, minor modifications

analysis/metric_space.lean

@@ -971,14 +971,16 @@ end
 instance complete_of_proper {α : Type u} [metric_space α] [proper_space α] : complete_space α :=
 ⟨begin
   intros f hf,
-  /-We want to show that the Cauchy filter `f` is converging. It suffices to find a closed
-  ball (therefore compact by properness) where it is nontrivial.-/
+  /- We want to show that the Cauchy filter `f` is converging. It suffices to find a closed
+  ball (therefore compact by properness) where it is nontrivial. -/
   have A : ∃ t ∈ f.sets, ∀ x y ∈ t, dist x y < 1 := (cauchy_of_metric.1 hf).2 1 zero_lt_one,
   rcases A with ⟨t, ⟨t_fset, ht⟩⟩,
   rcases inhabited_of_mem_sets hf.1 t_fset with ⟨x, xt⟩,
   have : t ⊆ closed_ball x 1 := by intros y yt; simp [dist_comm]; apply le_of_lt (ht x y xt yt),
   have : closed_ball x 1 ∈ f.sets := f.sets_of_superset t_fset this,
-  exact complete_of_compact_set hf this (proper_space.compact_ball _ _),
+  rcases (compact_iff_totally_bounded_complete.1 (proper_space.compact_ball x 1)).2 f hf (le_principal_iff.2 this)
+    with ⟨y, _, hy⟩,
+  exact ⟨y, hy⟩
 end⟩
 
 /-- A proper metric space is separable, and therefore second countable. Indeed, any ball is

analysis/topology/infinite_sum.lean

@@ -147,7 +147,7 @@ mem_at_top_sets.mpr $ exists.intro fsts $ assume bs (hbs : fsts ⊆ bs),
     from tendsto_finset_sum bs $
       assume c hc, tendsto_infi' c $ tendsto_infi' hc $ tendsto_comap.comp (hf c),
   have bs.sum g ∈ s,
-    from mem_closure_of_tendsto this hsc $ forall_sets_neq_empty_iff_neq_bot.mp $
+    from mem_of_closed_of_tendsto' this hsc $ forall_sets_neq_empty_iff_neq_bot.mp $
       by simp [mem_inf_sets, exists_imp_distrib, and_imp, forall_and_distrib,
                filter.mem_infi_sets_finset, mem_comap_sets, skolem, mem_at_top_sets,
                and_comm];
@@ -379,7 +379,7 @@ variables [ordered_comm_monoid α] [topological_space α] [ordered_topology α]
 variables {f g : β → α} {a a₁ a₂ : α}
 
 lemma is_sum_le (h : ∀b, f b ≤ g b) (hf : is_sum f a₁) (hg : is_sum g a₂) : a₁ ≤ a₂ :=
-le_of_tendsto at_top_ne_bot hf hg $ univ_mem_sets' $ assume s, sum_le_sum' $ assume b _, h b
+le_of_tendsto_of_tendsto at_top_ne_bot hf hg $ univ_mem_sets' $ assume s, sum_le_sum' $ assume b _, h b
 
 lemma tsum_le_tsum (h : ∀b, f b ≤ g b) (hf : has_sum f) (hg : has_sum g) : (∑b, f b) ≤ (∑b, g b) :=
 is_sum_le h (is_sum_tsum hf) (is_sum_tsum hg)

analysis/topology/topological_space.lean

@@ -223,6 +223,9 @@ lemma closure_subset_iff_subset_of_is_closed {s t : set α} (h₁ : is_closed t)
 lemma closure_mono {s t : set α} (h : s ⊆ t) : closure s ⊆ closure t :=
 closure_minimal (subset.trans h subset_closure) is_closed_closure
 
+lemma is_closed_of_closure_subset {s : set α} (h : closure s ⊆ s) : is_closed s :=
+by rw subset.antisymm subset_closure h; exact is_closed_closure
+
 @[simp] lemma closure_empty : closure (∅ : set α) = ∅ :=
 closure_eq_of_is_closed is_closed_empty
 
@@ -419,12 +422,17 @@ have b.map f ≤ nhds a ⊓ principal s,
   from le_trans (le_inf (le_refl _) (le_principal_iff.mpr h)) (inf_le_inf hf (le_refl _)),
 is_closed_iff_nhds.mp hs a $ neq_bot_of_le_neq_bot (map_ne_bot hb) this
 
-lemma mem_closure_of_tendsto {f : β → α} {x : filter β} {a : α} {s : set α}
+lemma mem_of_closed_of_tendsto' {f : β → α} {x : filter β} {a : α} {s : set α}
   (hf : tendsto f x (nhds a)) (hs : is_closed s) (h : x ⊓ principal (f ⁻¹' s) ≠ ⊥) : a ∈ s :=
 is_closed_iff_nhds.mp hs _ $ neq_bot_of_le_neq_bot (@map_ne_bot _ _ _ f h) $
   le_inf (le_trans (map_mono $ inf_le_left) hf) $
     le_trans (map_mono $ inf_le_right_of_le $ by simp only [comap_principal, le_principal_iff]; exact subset.refl _) (@map_comap_le _ _ _ f)
 
+lemma mem_closure_of_tendsto {f : β → α} {b : filter β} {a : α} {s : set α}
+  (hb : b ≠ ⊥) (hf : tendsto f b (nhds a)) (h : f ⁻¹' s ∈ b.sets) : a ∈ closure s :=
+mem_of_closed_of_tendsto hb hf (is_closed_closure) $
+  filter.mem_sets_of_superset h (preimage_mono subset_closure)
+
 /- locally finite family [General Topology (Bourbaki, 1995)] -/
 section locally_finite
 

analysis/topology/topological_structures.lean

@@ -450,14 +450,22 @@ is_closed_le continuous_const continuous_id
 lemma is_closed_Icc {a b : α} : is_closed (Icc a b) :=
 is_closed_inter (is_closed_ge' a) (is_closed_le' b)
 
-lemma le_of_tendsto {f g : β → α} {b : filter β} {a₁ a₂ : α} (hb : b ≠ ⊥)
+lemma le_of_tendsto_of_tendsto {f g : β → α} {b : filter β} {a₁ a₂ : α} (hb : b ≠ ⊥)
   (hf : tendsto f b (nhds a₁)) (hg : tendsto g b (nhds a₂)) (h : {b | f b ≤ g b} ∈ b.sets) :
   a₁ ≤ a₂ :=
 have tendsto (λb, (f b, g b)) b (nhds (a₁, a₂)),
   by rw [nhds_prod_eq]; exact hf.prod_mk hg,
 show (a₁, a₂) ∈ {p:α×α | p.1 ≤ p.2},
   from mem_of_closed_of_tendsto hb this t.is_closed_le' h
 
+lemma le_of_tendsto {f : β → α} {a b : α} {x : filter β}
+  (nt : x ≠ ⊥) (lim : tendsto f x (nhds a)) (h : f ⁻¹' {c | c ≤ b} ∈ x.sets) : a ≤ b :=
+le_of_tendsto_of_tendsto nt lim tendsto_const_nhds h
+
+lemma ge_of_tendsto {f : β → α} {a b : α} {x : filter β}
+  (nt : x ≠ ⊥) (lim : tendsto f x (nhds a)) (h : f ⁻¹' {c | b ≤ c} ∈ x.sets) : b ≤ a :=
+le_of_tendsto_of_tendsto nt tendsto_const_nhds lim h
+
 @[simp] lemma closure_le_eq [topological_space β] {f g : β → α} (hf : continuous f) (hg : continuous g) :
   closure {b | f b ≤ g b} = {b | f b ≤ g b} :=
 closure_eq_iff_is_closed.mpr $ is_closed_le hf hg
@@ -949,7 +957,7 @@ have ∀a'∈s, ¬ b < f a',
       lt_irrefl _ (lt_of_le_of_lt ha'x hxa')),
 and.intro
   (assume b' ⟨a', ha', h_eq⟩, h_eq ▸ not_lt.1 $ this _ ha')
-  (assume b' hb', le_of_tendsto hnbot hb tendsto_const_nhds $
+  (assume b' hb', le_of_tendsto hnbot hb $
       mem_inf_sets_of_right $ assume x hx, hb' _ $ mem_image_of_mem _ hx)
 
 lemma is_glb_of_is_glb_of_tendsto {f : α → β} {s : set α} {a : α} {b : β}
@@ -977,7 +985,7 @@ have ∀a'∈s, ¬ b > f a',
       lt_irrefl _ (lt_of_lt_of_le hxa' ha'x)),
 and.intro
   (assume b' ⟨a', ha', h_eq⟩, h_eq ▸ not_lt.1 $ this _ ha')
-  (assume b' hb', le_of_tendsto hnbot tendsto_const_nhds hb $
+  (assume b' hb', ge_of_tendsto hnbot hb $
       mem_inf_sets_of_right $ assume x hx, hb' _ $ mem_image_of_mem _ hx)
 
 lemma is_glb_of_is_lub_of_tendsto {f : α → β} {s : set α} {a : α} {b : β}
@@ -1005,7 +1013,7 @@ have ∀a'∈s, ¬ b > f a',
       lt_irrefl _ (lt_of_lt_of_le hxa' ha'x)),
 and.intro
   (assume b' ⟨a', ha', h_eq⟩, h_eq ▸ not_lt.1 $ this _ ha')
-  (assume b' hb', le_of_tendsto hnbot tendsto_const_nhds hb $
+  (assume b' hb', ge_of_tendsto hnbot hb $
       mem_inf_sets_of_right $ assume x hx, hb' _ $ mem_image_of_mem _ hx)
 
 lemma mem_closure_of_is_lub {a : α} {s : set α} (ha : is_lub s a) (hs : s ≠ ∅) : a ∈ closure s :=
@@ -1074,31 +1082,49 @@ lemma Inf_mem_of_is_closed {α : Type u} [topological_space α] [complete_linear
   {s : set α} (hs : s ≠ ∅) (hc : is_closed s) : Inf s ∈ s :=
 mem_of_is_glb_of_is_closed  is_glb_Inf hs hc
 
-/-- A continuous monotone function sends supremum to supremum. -/
-lemma Sup_of_Sup_of_monotone_of_continuous {f : α → β} (Mf : continuous f) (Cf : monotone f)
+/-- A continuous monotone function sends supremum to supremum for nonempty sets. -/
+lemma Sup_of_Sup_of_monotone_of_continuous_of_nonempty {f : α → β} (Mf : continuous f) (Cf : monotone f)
   {s : set α} (hs : s ≠ ∅) : f (Sup s) = Sup (f '' s) :=
 --This is a particular case of the more general is_lub_of_is_lub_of_tendsto
 (is_lub_iff_Sup_eq.1
   (is_lub_of_is_lub_of_tendsto (λ x hx y hy xy, Cf xy) is_lub_Sup hs $
     tendsto_le_left inf_le_left (continuous.tendsto Mf _))).symm
 
+/-- A continuous monotone function sending bot to bot sends supremum to supremum. -/
+lemma Sup_of_Sup_of_monotone_of_continuous {f : α → β} (Mf : continuous f) (Cf : monotone f)
+  (fbot : f ⊥ = ⊥) {s : set α} : f (Sup s) = Sup (f '' s) :=
+begin
+  by_cases (s = ∅),
+  { simpa [h] },
+  { exact Sup_of_Sup_of_monotone_of_continuous_of_nonempty Mf Cf h }
+end
+
 /-- A continuous monotone function sends indexed supremum to indexed supremum. -/
 lemma supr_of_supr_of_monotone_of_continuous {f : α → β} {g : γ → α}
   (Mf : continuous f) (Cf : monotone f) : f (supr g) = supr (f ∘ g) :=
-by rw [supr, Sup_of_Sup_of_monotone_of_continuous Mf Cf
+by rw [supr, Sup_of_Sup_of_monotone_of_continuous_of_nonempty Mf Cf
   (λ h, range_eq_empty.1 h ‹_›), ← range_comp]; refl
 
-/-- A continuous monotone function sends infimum to infimum. -/
-lemma Inf_of_Inf_of_monotone_of_continuous {f : α → β} (Mf : continuous f) (Cf : monotone f)
+/-- A continuous monotone function sends infimum to infimum for nonempty sets. -/
+lemma Inf_of_Inf_of_monotone_of_continuous_of_nonempty {f : α → β} (Mf : continuous f) (Cf : monotone f)
   {s : set α} (hs : s ≠ ∅) : f (Inf s) = Inf (f '' s) :=
 (is_glb_iff_Inf_eq.1
   (is_glb_of_is_glb_of_tendsto (λ x hx y hy xy, Cf xy) is_glb_Inf hs $
     tendsto_le_left inf_le_left (continuous.tendsto Mf _))).symm
 
+/-- A continuous monotone function sending top to top sends infimum to infimum. -/
+lemma Inf_of_Inf_of_monotone_of_continuous {f : α → β} (Mf : continuous f) (Cf : monotone f)
+  (ftop : f ⊤ = ⊤) {s : set α} : f (Inf s) = Inf (f '' s) :=
+begin
+  by_cases (s = ∅),
+  { simpa [h] },
+  { exact Inf_of_Inf_of_monotone_of_continuous_of_nonempty Mf Cf h }
+end
+
 /-- A continuous monotone function sends indexed infimum to indexed infimum. -/
 lemma infi_of_infi_of_monotone_of_continuous {f : α → β} {g : γ → α}
   (Mf : continuous f) (Cf : monotone f) : f (infi g) = infi (f ∘ g) :=
-by rw [infi, Inf_of_Inf_of_monotone_of_continuous Mf Cf
+by rw [infi, Inf_of_Inf_of_monotone_of_continuous_of_nonempty Mf Cf
   (λ h, range_eq_empty.1 h ‹_›), ← range_comp]; refl
 
 end complete_linear_order