refactor(order/filter/bases): drop p in has_antitone_basis (#10499)

We never use `has_antitone_basis` for `p ≠ λ _, true` in `mathlib`.



Co-authored-by: Patrick Massot <patrickmassot@free.fr>

src/order/filter/at_top_bot.lean

@@ -1220,50 +1220,42 @@ from (le_infi $ assume b, let ⟨v, hv⟩ := h_eq b in infi_le_of_le v $
   by simp [set.image_subset_iff]; exact hv)
 
 lemma has_antitone_basis.tendsto [semilattice_sup ι] [nonempty ι] {l : filter α}
-  {p : ι → Prop} {s : ι → set α} (hl : l.has_antitone_basis p s) {φ : ι → α}
+  {s : ι → set α} (hl : l.has_antitone_basis s) {φ : ι → α}
   (h : ∀ i : ι, φ i ∈ s i) : tendsto φ at_top l  :=
 (at_top_basis.tendsto_iff hl.to_has_basis).2 $ assume i hi,
-  ⟨i, trivial, λ j hij, hl.decreasing hi (hl.mono hij hi) hij (h j)⟩
+  ⟨i, trivial, λ j hij, hl.antitone hij (h _)⟩
+
+/-- If `f` is a nontrivial countably generated filter, then there exists a sequence that converges
+to `f`. -/
+lemma exists_seq_tendsto (f : filter α) [is_countably_generated f] [ne_bot f] :
+  ∃ x : ℕ → α, tendsto x at_top f :=
+begin
+  obtain ⟨B, h⟩ := f.exists_antitone_basis,
+  have := λ n, nonempty_of_mem (h.to_has_basis.mem_of_mem trivial : B n ∈ f), choose x hx,
+  exact ⟨x, h.tendsto hx⟩
+end
 
 /-- An abstract version of continuity of sequentially continuous functions on metric spaces:
 if a filter `k` is countably generated then `tendsto f k l` iff for every sequence `u`
 converging to `k`, `f ∘ u` tends to `l`. -/
 lemma tendsto_iff_seq_tendsto {f : α → β} {k : filter α} {l : filter β} [k.is_countably_generated] :
   tendsto f k l ↔ (∀ x : ℕ → α, tendsto x at_top k → tendsto (f ∘ x) at_top l) :=
-suffices (∀ x : ℕ → α, tendsto x at_top k → tendsto (f ∘ x) at_top l) → tendsto f k l,
-  from ⟨by intros; apply tendsto.comp; assumption, by assumption⟩,
 begin
-  obtain ⟨g, gbasis, gmon, -⟩ := k.exists_antitone_basis,
-  contrapose,
-  simp only [not_forall, gbasis.tendsto_left_iff, exists_const, not_exists, not_imp],
-  rintro ⟨B, hBl, hfBk⟩,
-  choose x h using hfBk,
-  use x, split,
-  { exact (at_top_basis.tendsto_iff gbasis).2
-      (λ i _, ⟨i, trivial, λ j hj, gmon trivial trivial hj (h j).1⟩) },
-  { simp only [tendsto_at_top', (∘), not_forall, not_exists],
-    use [B, hBl],
-    intro i, use [i, (le_refl _)],
-    apply (h i).right },
+  refine ⟨λ h x hx, h.comp hx, λ H s hs, _⟩,
+  contrapose! H,
+  haveI : ne_bot (k ⊓ 𝓟 (f ⁻¹' sᶜ)), by simpa [ne_bot_iff,  inf_principal_eq_bot],
+  rcases (k ⊓ 𝓟 (f ⁻¹' sᶜ)).exists_seq_tendsto with ⟨x, hx⟩,
+  rw [tendsto_inf, tendsto_principal] at hx,
+  refine ⟨x, hx.1, λ h, _⟩,
+  rcases (hx.2.and (h hs)).exists with ⟨N, hnmem, hmem⟩,
+  exact hnmem hmem
 end
 
 lemma tendsto_of_seq_tendsto {f : α → β} {k : filter α} {l : filter β} [k.is_countably_generated] :
   (∀ x : ℕ → α, tendsto x at_top k → tendsto (f ∘ x) at_top l) → tendsto f k l :=
 tendsto_iff_seq_tendsto.2
 
-/-- If `f` is a nontrivial countably generated basis, then there exists a sequence that converges
-to `f`. -/
-lemma exists_seq_tendsto (f : filter α) [is_countably_generated f] [ne_bot f] :
-  ∃ x : ℕ → α, tendsto x at_top f :=
-begin
-  obtain ⟨B, h, h_mono, -⟩ := f.exists_antitone_basis,
-  have := λ n, nonempty_of_mem (h.mem_of_mem trivial : B n ∈ f), choose x hx,
-  exact ⟨x, h.tendsto_right_iff.2 $
-    λ n hn, eventually_at_top.2 ⟨n, λ m hm, h_mono trivial trivial hm (hx m)⟩⟩
-end
-
-lemma subseq_tendsto_of_ne_bot {f : filter α} [is_countably_generated f]
-  {u : ℕ → α}
+lemma subseq_tendsto_of_ne_bot {f : filter α} [is_countably_generated f] {u : ℕ → α}
   (hx : ne_bot (f ⊓ map u at_top)) :
   ∃ (θ : ℕ → ℕ), (strict_mono θ) ∧ (tendsto (u ∘ θ) at_top f) :=
 begin

src/order/filter/bases.lean

@@ -593,21 +593,17 @@ begin
     exact sub (h i hi) },
 end
 
-variables {ι'' : Type*} [preorder ι''] (l) (p'' : ι'' → Prop) (s'' : ι'' → set α)
-
-/-- `is_antitone_basis p s` means the image of `s` bounded by `p` is a filter basis
-such that `s` is decreasing and `p` is increasing, ie `i ≤ j → p i → p j`. -/
-structure is_antitone_basis extends is_basis p'' s'' : Prop :=
-(decreasing : ∀ {i j}, p'' i → p'' j → i ≤ j → s'' j ⊆ s'' i)
-(mono : monotone p'')
-
-/-- We say that a filter `l` has an antitone basis `s : ι → set α` bounded by `p : ι → Prop`,
-if `t ∈ l` if and only if `t` includes `s i` for some `i` such that `p i`,
-and `s` is decreasing and `p` is increasing, ie `i ≤ j → p i → p j`. -/
-structure has_antitone_basis (l : filter α) (p : ι'' → Prop) (s : ι'' → set α)
-  extends has_basis l p s : Prop :=
-(decreasing : ∀ {i j}, p i → p j → i ≤ j → s j ⊆ s i)
-(mono : monotone p)
+variables {ι'' : Type*} [preorder ι''] (l) (s'' : ι'' → set α)
+
+/-- `is_antitone_basis s` means the image of `s` is a filter basis such that `s` is decreasing. -/
+@[protect_proj] structure is_antitone_basis extends is_basis (λ _, true) s'' : Prop :=
+(antitone : antitone s'')
+
+/-- We say that a filter `l` has an antitone basis `s : ι → set α`, if `t ∈ l` if and only if `t`
+includes `s i` for some `i`, and `s` is decreasing. -/
+@[protect_proj] structure has_antitone_basis (l : filter α) (s : ι'' → set α)
+  extends has_basis l (λ _, true) s : Prop :=
+(antitone : antitone s)
 
 end same_type
 
@@ -707,7 +703,7 @@ lemma has_countable_basis.is_countably_generated {f : filter α} {p : ι → Pro
 ⟨⟨{t | ∃ i, p i ∧ s i = t}, h.countable.image s, h.to_has_basis.eq_generate⟩⟩
 
 lemma antitone_seq_of_seq (s : ℕ → set α) :
-  ∃ t : ℕ → set α, (∀ i j, i ≤ j → t j ⊆ t i) ∧ (⨅ i, 𝓟 $ s i) = ⨅ i, 𝓟 (t i) :=
+  ∃ t : ℕ → set α, antitone t ∧ (⨅ i, 𝓟 $ s i) = ⨅ i, 𝓟 (t i) :=
 begin
   use λ n, ⋂ m ≤ n, s m, split,
   { exact λ i j hij, bInter_mono' (Iic_subset_Iic.2 hij) (λ n hn, subset.refl _) },
@@ -752,7 +748,7 @@ sequence `i n` such that `p (i n)` for all `n` and `s (i n)` is a decreasing seq
 forms a basis of `f`-/
 lemma has_basis.exists_antitone_subbasis {f : filter α} [h : f.is_countably_generated]
   {p : ι → Prop} {s : ι → set α} (hs : f.has_basis p s) :
-  ∃ x : ℕ → ι, (∀ i, p (x i)) ∧ f.has_antitone_basis (λ _, true) (λ i, s (x i)) :=
+  ∃ x : ℕ → ι, (∀ i, p (x i)) ∧ f.has_antitone_basis (λ i, s (x i)) :=
 begin
   obtain ⟨x', hx'⟩ : ∃ x : ℕ → set α, f = ⨅ i, 𝓟 (x i),
   { unfreezingI { rcases h with ⟨s, hsc, rfl⟩ },
@@ -768,8 +764,8 @@ begin
   { rintro (_|i),
     exacts [hs.set_index_subset _, subset.trans (hs.set_index_subset _) (inter_subset_left _ _)] },
   refine ⟨λ i, x i, λ i, (x i).2, _⟩,
-  have : (⨅ i, 𝓟 (s (x i))).has_antitone_basis (λ _, true) (λ i, s (x i)) :=
-    ⟨has_basis_infi_principal (directed_of_sup x_mono), λ i j _ _ hij, x_mono hij, monotone_const⟩,
+  have : (⨅ i, 𝓟 (s (x i))).has_antitone_basis (λ i, s (x i)) :=
+    ⟨has_basis_infi_principal (directed_of_sup x_mono), x_mono⟩,
   convert this,
   exact le_antisymm (le_infi $ λ i, le_principal_iff.2 $ by cases i; apply hs.set_index_mem)
     (hx'.symm ▸ le_infi (λ i, le_principal_iff.2 $
@@ -778,18 +774,13 @@ end
 
 /-- A countably generated filter admits a basis formed by an antitone sequence of sets. -/
 lemma exists_antitone_basis (f : filter α) [f.is_countably_generated] :
-  ∃ x : ℕ → set α, f.has_antitone_basis (λ _, true) x :=
+  ∃ x : ℕ → set α, f.has_antitone_basis x :=
 let ⟨x, hxf, hx⟩ := f.basis_sets.exists_antitone_subbasis in ⟨x, hx⟩
 
-lemma exists_antitone_eq_infi_principal (f : filter α) [f.is_countably_generated] :
-  ∃ x : ℕ → set α, antitone x ∧ f = ⨅ n, 𝓟 (x n) :=
-let ⟨x, hxf⟩ := f.exists_antitone_basis
-in ⟨x, λ i j, hxf.decreasing trivial trivial, hxf.to_has_basis.eq_infi⟩
-
 lemma exists_antitone_seq (f : filter α) [f.is_countably_generated] :
   ∃ x : ℕ → set α, antitone x ∧ ∀ {s}, (s ∈ f ↔ ∃ i, x i ⊆ s) :=
 let ⟨x, hx⟩ := f.exists_antitone_basis in
-⟨x, λ i j, hx.decreasing trivial trivial, λ s, by simp [hx.to_has_basis.mem_iff]⟩
+⟨x, hx.antitone, λ s, by simp [hx.to_has_basis.mem_iff]⟩
 
 instance inf.is_countably_generated (f g : filter α) [is_countably_generated f]
   [is_countably_generated g] :
@@ -834,7 +825,7 @@ lemma is_countably_generated_binfi_principal {B : set $ set α} (h : countable B
 is_countably_generated_of_seq (countable_binfi_principal_eq_seq_infi h)
 
 lemma is_countably_generated_iff_exists_antitone_basis {f : filter α} :
-  is_countably_generated f ↔ ∃ x : ℕ → set α, f.has_antitone_basis (λ _, true) x :=
+  is_countably_generated f ↔ ∃ x : ℕ → set α, f.has_antitone_basis x :=
 begin
   split,
   { introI h, exact f.exists_antitone_basis },

src/topology/G_delta.lean

@@ -109,7 +109,7 @@ end
 lemma is_closed.is_Gδ {α} [uniform_space α] [is_countably_generated (𝓤 α)]
   {s : set α} (hs : is_closed s) : is_Gδ s :=
 begin
-  rcases (@uniformity_has_basis_open α _).exists_antitone_subbasis  with ⟨U, hUo, hU, -, -⟩,
+  rcases (@uniformity_has_basis_open α _).exists_antitone_subbasis  with ⟨U, hUo, hU, -⟩,
   rw [← hs.closure_eq, ← hU.bInter_bUnion_ball],
   refine is_Gδ_bInter (countable_encodable _) (λ n hn, is_open.is_Gδ _),
   exact is_open_bUnion (λ x hx, uniform_space.is_open_ball _ (hUo _).2)

src/topology/sequences.lean

@@ -240,7 +240,7 @@ lemma lebesgue_number_lemma_seq {ι : Type*} [is_countably_generated (𝓤 β)]
 begin
   classical,
   obtain ⟨V, hV, Vsymm⟩ :
-    ∃ V : ℕ → set (β × β), (𝓤 β).has_antitone_basis (λ _, true) V ∧  ∀ n, swap ⁻¹' V n = V n,
+    ∃ V : ℕ → set (β × β), (𝓤 β).has_antitone_basis V ∧ ∀ n, swap ⁻¹' V n = V n,
       from uniform_space.has_seq_basis β,
   suffices : ∃ n, ∀ x ∈ s, ∃ i, ball x (V n) ⊆ c i,
   { cases this with n hn,
@@ -268,10 +268,10 @@ begin
     obtain ⟨N₂, h₂⟩ : ∃ N₂, V (φ N₂) ⊆ W,
     { rcases hV.to_has_basis.mem_iff.mp W_in with ⟨N, _, hN⟩,
       use N,
-      exact subset.trans (hV.decreasing trivial trivial $  φ_mono.id_le _) hN },
+      exact subset.trans (hV.antitone $ φ_mono.id_le _) hN },
     have : φ N₂ ≤ φ (max N₁ N₂),
       from φ_mono.le_iff_le.mpr (le_max_right _ _),
-    exact ⟨max N₁ N₂, h₁ _ (le_max_left _ _), trans (hV.decreasing trivial trivial this) h₂⟩ },
+    exact ⟨max N₁ N₂, h₁ _ (le_max_left _ _), trans (hV.antitone this) h₂⟩ },
   suffices : ball (x (φ N)) (V (φ N)) ⊆ c i₀,
     from hx (φ N) i₀ this,
   calc

src/topology/uniform_space/basic.lean

@@ -875,7 +875,7 @@ section
 variable (α)
 
 lemma uniform_space.has_seq_basis [is_countably_generated $ 𝓤 α] :
-  ∃ V : ℕ → set (α × α), has_antitone_basis (𝓤 α) (λ _, true) V ∧ ∀ n, symmetric_rel (V n) :=
+  ∃ V : ℕ → set (α × α), has_antitone_basis (𝓤 α) V ∧ ∀ n, symmetric_rel (V n) :=
 let ⟨U, hsym, hbasis⟩ :=  uniform_space.has_basis_symmetric.exists_antitone_subbasis
 in ⟨U, hbasis, λ n, (hsym n).2⟩
 

src/topology/uniform_space/cauchy.lean

@@ -614,21 +614,22 @@ begin
   rcases exists_countable_dense α with ⟨s, hsc, hsd⟩,
   obtain ⟨t : ℕ → set (α × α),
     hto : ∀ (i : ℕ), t i ∈ (𝓤 α).sets ∧ is_open (t i) ∧ symmetric_rel (t i),
-    h_basis : (𝓤 α).has_antitone_basis (λ _, true) t⟩ :=
+      h_basis : (𝓤 α).has_antitone_basis t⟩ :=
     (@uniformity_has_basis_open_symmetric α _).exists_antitone_subbasis,
+  choose ht_mem hto hts using hto,
   refine ⟨⟨⋃ (x ∈ s), range (λ k, ball x (t k)), hsc.bUnion (λ x hx, countable_range _), _⟩⟩,
   refine (is_topological_basis_of_open_of_nhds _ _).eq_generate_from,
   { simp only [mem_bUnion_iff, mem_range],
     rintros _ ⟨x, hxs, k, rfl⟩,
-    exact is_open_ball x (hto k).2.1 },
+    exact is_open_ball x (hto k) },
   { intros x V hxV hVo,
     simp only [mem_bUnion_iff, mem_range, exists_prop],
     rcases uniform_space.mem_nhds_iff.1 (is_open.mem_nhds hVo hxV) with ⟨U, hU, hUV⟩,
     rcases comp_symm_of_uniformity hU with ⟨U', hU', hsymm, hUU'⟩,
     rcases h_basis.to_has_basis.mem_iff.1 hU' with ⟨k, -, hk⟩,
-    rcases hsd.inter_open_nonempty (ball x $ t k) (uniform_space.is_open_ball x (hto k).2.1)
-      ⟨x, uniform_space.mem_ball_self _ (hto k).1⟩ with ⟨y, hxy, hys⟩,
-    refine ⟨_, ⟨y, hys, k, rfl⟩, (hto k).2.2.subset hxy, λ z hz, _⟩,
+    rcases hsd.inter_open_nonempty (ball x $ t k) (is_open_ball x (hto k))
+      ⟨x, uniform_space.mem_ball_self _ (ht_mem k)⟩ with ⟨y, hxy, hys⟩,
+    refine ⟨_, ⟨y, hys, k, rfl⟩, (hts k).subset hxy, λ z hz, _⟩,
     exact hUV (ball_subset_of_comp_subset (hk hxy) hUU' (hk hz)) }
 end