feat(topology/bornology/basic): alternate way of defining a bornology by its bounded set (#13064)

More precisely, this defines an alternative to https://leanprover-community.github.io/mathlib_docs/topology/bornology/basic.html#bornology.of_bounded (which is renamed `bornology.of_bounded'`) which expresses the covering condition as containing the singletons, and factors the old version trough it to have a simpler proof.

Note : I chose to add a prime to the old constructor because it's now defined in terms of the new one, so defeq works better this way (i.e lemma about the new constructor can be used whenever the old one is used).

Author: ADedecker

src/analysis/locally_convex/bounded.lean

@@ -114,7 +114,7 @@ metric bornology.-/
 @[reducible] -- See note [reducible non-instances]
 def vonN_bornology : bornology E :=
 bornology.of_bounded (set_of (is_vonN_bounded 𝕜)) (is_vonN_bounded_empty 𝕜 E)
-  (λ _ hs _ ht, hs.subset ht) (λ _ hs _, hs.union) is_vonN_bounded_covers
+  (λ _ hs _ ht, hs.subset ht) (λ _ hs _, hs.union) is_vonN_bounded_singleton
 
 variables {E}
 

src/order/filter/cofinite.lean

@@ -103,6 +103,14 @@ frequently_cofinite_iff_infinite.symm
 lemma filter.eventually_cofinite_ne (x : α) : ∀ᶠ a in cofinite, a ≠ x :=
 (set.finite_singleton x).eventually_cofinite_nmem
 
+lemma filter.le_cofinite_iff_compl_singleton_mem {l : filter α} :
+  l ≤ cofinite ↔ ∀ x, {x}ᶜ ∈ l :=
+begin
+  refine ⟨λ h x, h (finite_singleton x).compl_mem_cofinite, λ h s (hs : sᶜ.finite), _⟩,
+  rw [← compl_compl s, ← bUnion_of_singleton sᶜ, compl_Union₂,filter.bInter_mem hs],
+  exact λ x _, h x
+end
+
 /-- If `α` is a sup-semilattice with no maximal element, then `at_top ≤ cofinite`. -/
 lemma at_top_le_cofinite [semilattice_sup α] [no_max_order α] : (at_top : filter α) ≤ cofinite :=
 begin
@@ -170,4 +178,3 @@ lemma function.injective.tendsto_cofinite {α β : Type*} {f : α → β} (hf :
 lemma function.injective.nat_tendsto_at_top {f : ℕ → ℕ} (hf : injective f) :
   tendsto f at_top at_top :=
 nat.cofinite_eq_at_top ▸ hf.tendsto_cofinite
-

src/topology/bornology/basic.lean

@@ -54,7 +54,7 @@ and showing that they satisfy the appropriate conditions. -/
 @[simps]
 def bornology.of_bounded {α : Type*} (B : set (set α))
   (empty_mem : ∅ ∈ B) (subset_mem : ∀ s₁ ∈ B, ∀ s₂ : set α, s₂ ⊆ s₁ → s₂ ∈ B)
-  (union_mem : ∀ s₁ s₂ ∈ B, s₁ ∪ s₂ ∈ B) (sUnion_univ : ⋃₀ B = univ) :
+  (union_mem : ∀ s₁ s₂ ∈ B, s₁ ∪ s₂ ∈ B) (singleton_mem : ∀ x, {x} ∈ B) :
   bornology α :=
 { cobounded :=
   { sets := {s : set α | sᶜ ∈ B},
@@ -63,17 +63,28 @@ def bornology.of_bounded {α : Type*} (B : set (set α))
     inter_sets := λ x y hx hy, by simpa [compl_inter] using union_mem xᶜ hx yᶜ hy, },
   le_cofinite :=
   begin
-    refine le_def.mpr (λ s, _),
-    simp only [mem_set_of_eq, mem_cofinite, filter.mem_mk],
-    generalize : sᶜ = s',
-    refine λ h, h.dinduction_on _ (λ x t hx ht h, _),
-    { exact empty_mem, },
-    { refine insert_eq x t ▸ union_mem _ _ _ h,
-      obtain ⟨b, hb : b ∈ B, hxb : x ∈ b⟩ :=
-        mem_sUnion.mp (by simpa [←sUnion_univ] using mem_univ x),
-      exact subset_mem _ hb _ (singleton_subset_iff.mpr hxb) },
+    rw le_cofinite_iff_compl_singleton_mem,
+    intros x,
+    change {x}ᶜᶜ ∈ B,
+    rw compl_compl,
+    exact singleton_mem x
   end }
 
+/-- A constructor for bornologies by specifying the bounded sets,
+and showing that they satisfy the appropriate conditions. -/
+@[simps]
+def bornology.of_bounded' {α : Type*} (B : set (set α))
+  (empty_mem : ∅ ∈ B) (subset_mem : ∀ s₁ ∈ B, ∀ s₂ : set α, s₂ ⊆ s₁ → s₂ ∈ B)
+  (union_mem : ∀ s₁ s₂ ∈ B, s₁ ∪ s₂ ∈ B) (sUnion_univ : ⋃₀ B = univ) :
+  bornology α :=
+bornology.of_bounded B empty_mem subset_mem union_mem
+  begin
+    rw eq_univ_iff_forall at sUnion_univ,
+    intros x,
+    rcases sUnion_univ x with ⟨s, hs, hxs⟩,
+    exact subset_mem s hs {x} (singleton_subset_iff.mpr hxs)
+  end
+
 namespace bornology
 
 section
@@ -101,6 +112,9 @@ alias is_cobounded_compl_iff ↔ bornology.is_cobounded.of_compl bornology.is_bo
 @[simp] lemma is_bounded_empty : is_bounded (∅ : set α) :=
 by { rw [is_bounded_def, compl_empty], exact univ_mem}
 
+@[simp] lemma is_bounded_singleton {x : α} : is_bounded ({x} : set α) :=
+by {rw [is_bounded_def], exact le_cofinite _ (finite_singleton x).compl_mem_cofinite}
+
 lemma is_bounded.union (h₁ : is_bounded s₁) (h₂ : is_bounded s₂) : is_bounded (s₁ ∪ s₂) :=
 by { rw [is_bounded_def, compl_union], exact (cobounded α).inter_sets h₁ h₂ }