feat(topology/subset_properties): define filter.cocompact (#4666)

The filter of complements to compact subsets.

src/analysis/normed_space/basic.lean

@@ -82,6 +82,10 @@ normed_group.dist_eq _ _
 @[simp] lemma dist_zero_right (g : α) : dist g 0 = ∥g∥ :=
 by rw [dist_eq_norm, sub_zero]
 
+lemma tendsto_norm_cocompact_at_top [proper_space α] :
+  tendsto norm (cocompact α) at_top :=
+by simpa only [dist_zero_right] using tendsto_dist_right_cocompact_at_top (0:α)
+
 lemma norm_sub_rev (g h : α) : ∥g - h∥ = ∥h - g∥ :=
 by simpa only [dist_eq_norm] using dist_comm g h
 
@@ -408,6 +412,10 @@ lemma filter.tendsto.norm {β : Type*} {l : filter β} {f : β → α} {a : α}
   tendsto (λ x, ∥f x∥) l (𝓝 ∥a∥) :=
 tendsto.comp continuous_norm.continuous_at h
 
+lemma continuous.norm [topological_space γ] {f : γ → α} (hf : continuous f) :
+  continuous (λ x, ∥f x∥) :=
+continuous_norm.comp hf
+
 lemma continuous_nnnorm : continuous (nnnorm : α → nnreal) :=
 continuous_subtype_mk _ continuous_norm
 
@@ -471,7 +479,7 @@ attribute [simp] norm_one
 @[simp] lemma nnnorm_one [normed_group α] [has_one α] [norm_one_class α] : nnnorm (1:α) = 1 :=
 nnreal.eq norm_one
 
-@[priority 100]
+@[priority 100] -- see Note [lower instance priority]
 instance normed_comm_ring.to_comm_ring [β : normed_comm_ring α] : comm_ring α := { ..β }
 
 @[priority 100] -- see Note [lower instance priority]

src/data/set/basic.lean

@@ -311,6 +311,8 @@ lemma nonempty_iff_univ_nonempty : nonempty α ↔ (univ : set α).nonempty :=
 lemma nonempty.to_subtype (h : s.nonempty) : nonempty s :=
 nonempty_subtype.2 h
 
+@[simp] lemma nonempty_insert (a : α) (s : set α) : (insert a s).nonempty := ⟨a, or.inl rfl⟩
+
 /-! ### Lemmas about the empty set -/
 
 theorem empty_def : (∅ : set α) = {x | false} := rfl

src/topology/algebra/ordered.lean

@@ -2271,6 +2271,15 @@ lemma is_compact.exists_Inf_image_eq {α : Type u} [topological_space α]
 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 u} [topological_space α]:
+  ∀ {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 β) _ _ _ _ _
+
+lemma eq_Icc_of_connected_compact {s : set α} (h₁ : is_connected s) (h₂ : is_compact s) :
+  s = Icc (Inf s) (Sup s) :=
+eq_Icc_cInf_cSup_of_connected_bdd_closed h₁ h₂.bdd_below h₂.bdd_above h₂.is_closed
+
 /-- The extreme value theorem: a continuous function realizes its minimum on a compact set -/
 lemma is_compact.exists_forall_le {α : Type u} [topological_space α]
   {s : set α} (hs : is_compact s) (ne_s : s.nonempty) {f : α → β} (hf : continuous_on f s) :
@@ -2288,15 +2297,28 @@ lemma is_compact.exists_forall_ge {α : Type u} [topological_space α]:
   ∃x∈s, ∀y∈s, f y ≤ f x :=
 @is_compact.exists_forall_le (order_dual β) _ _ _ _ _
 
-lemma is_compact.exists_Sup_image_eq {α : Type u} [topological_space α]:
-  ∀ {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 β) _ _ _ _ _
-
-lemma eq_Icc_of_connected_compact {s : set α} (h₁ : is_connected s) (h₂ : is_compact s) :
-  s = Icc (Inf s) (Sup s) :=
-eq_Icc_cInf_cSup_of_connected_bdd_closed h₁ h₂.bdd_below h₂.bdd_above
-  h₂.is_closed
+/-- 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) :
+  ∃ 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,
+  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
+compactx 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) :
+  ∃ x, ∀ y, f y ≤ f x :=
+@continuous.exists_forall_le (order_dual β) _ _ _ _ _ _ _ hf hlim
 
 end conditionally_complete_linear_order
 

src/topology/metric_space/basic.lean

@@ -1210,6 +1210,15 @@ open metric
 class proper_space (α : Type u) [metric_space α] : Prop :=
 (compact_ball : ∀x:α, ∀r, is_compact (closed_ball x r))
 
+lemma tendsto_dist_right_cocompact_at_top [proper_space α] (x : α) :
+  tendsto (λ y, dist y x) (cocompact α) at_top :=
+(has_basis_cocompact.tendsto_iff at_top_basis).2 $ λ r hr,
+  ⟨closed_ball x r, proper_space.compact_ball x r, λ y hy, (not_le.1 $ mt mem_closed_ball.2 hy).le⟩
+
+lemma tendsto_dist_left_cocompact_at_top [proper_space α] (x : α) :
+  tendsto (dist x) (cocompact α) at_top :=
+by simpa only [dist_comm] using tendsto_dist_right_cocompact_at_top x
+
 /-- If all closed balls of large enough radius are compact, then the space is proper. Especially
 useful when the lower bound for the radius is 0. -/
 lemma proper_space_of_compact_closed_ball_of_le
@@ -1230,7 +1239,7 @@ end⟩
 /- A compact metric space is proper -/
 @[priority 100] -- see Note [lower instance priority]
 instance proper_of_compact [compact_space α] : proper_space α :=
-⟨assume x r, compact_of_is_closed_subset compact_univ is_closed_ball (subset_univ _)⟩
+⟨assume x r, is_closed_ball.compact⟩
 
 /-- A proper space is locally compact -/
 @[priority 100] -- see Note [lower instance priority]

src/topology/separation.lean

@@ -304,6 +304,7 @@ lemma compact_compact_separated [t2_space α] {s t : set α}
 by simp only [prod_subset_compl_diagonal_iff_disjoint.symm] at ⊢ hst;
    exact generalized_tube_lemma hs ht is_closed_diagonal hst
 
+/-- In a `t2_space`, every compact set is closed. -/
 lemma is_compact.is_closed [t2_space α] {s : set α} (hs : is_compact s) : is_closed s :=
 is_open_compl_iff.mpr $ is_open_iff_forall_mem_open.mpr $ assume x hx,
   let ⟨u, v, uo, vo, su, xv, uv⟩ :=

src/topology/subset_properties.lean

@@ -299,9 +299,8 @@ empty_in_sets_eq_bot.1 $ le_principal_iff.1 hsf
 
 @[simp]
 lemma compact_singleton {a : α} : is_compact ({a} : set α) :=
-compact_of_finite_subcover $ assume ι U hUo hsU,
-  let ⟨i, hai⟩ := (show ∃i : ι, a ∈ U i, from mem_Union.1 $ singleton_subset_iff.1 hsU) in
-  ⟨{i}, singleton_subset_iff.2 (by simpa only [finset.bUnion_singleton])⟩
+λ f hf hfa, ⟨a, rfl, cluster_pt.of_le_nhds'
+  (hfa.trans $ by simpa only [principal_singleton] using pure_le_nhds a) hf⟩
 
 lemma set.finite.compact_bUnion {s : set β} {f : β → set α} (hs : finite s)
   (hf : ∀i ∈ s, is_compact (f i)) :
@@ -331,6 +330,27 @@ bUnion_of_singleton s ▸ hs.compact_bUnion (λ _ _, compact_singleton)
 lemma is_compact.union (hs : is_compact s) (ht : is_compact t) : is_compact (s ∪ t) :=
 by rw union_eq_Union; exact compact_Union (λ b, by cases b; assumption)
 
+lemma is_compact.insert (hs : is_compact s) (a) : is_compact (insert a s) :=
+compact_singleton.union hs
+
+/-- `filter.cocompact` is the filter generated by complements to compact sets. -/
+def filter.cocompact (α : Type*) [topological_space α] : filter α :=
+⨅ (s : set α) (hs : is_compact s), 𝓟 (sᶜ)
+lemma filter.has_basis_cocompact : (filter.cocompact α).has_basis is_compact compl :=
+has_basis_binfi_principal'
+  (λ s hs t ht, ⟨s ∪ t, hs.union ht, compl_subset_compl.2 (subset_union_left s t),
+    compl_subset_compl.2 (subset_union_right s t)⟩)
+  ⟨∅, compact_empty⟩
+
+lemma filter.mem_cocompact : s ∈ filter.cocompact α ↔ ∃ t, is_compact t ∧ tᶜ ⊆ s :=
+filter.has_basis_cocompact.mem_iff.trans $ exists_congr $ λ t,  exists_prop
+
+lemma filter.mem_cocompact' : s ∈ filter.cocompact α ↔ ∃ t, is_compact t ∧ sᶜ ⊆ t :=
+filter.mem_cocompact.trans $ exists_congr $ λ t, and_congr_right $ λ ht, compl_subset_comm
+
+lemma is_compact.compl_mem_cocompact (hs : is_compact s) : sᶜ ∈ filter.cocompact α :=
+filter.has_basis_cocompact.mem_of_mem hs
+
 section tube_lemma
 
 variables [topological_space β]