feat(order/filter/bases): define filter.has_basis (#1896)

* feat(*): assorted simple lemmas, simplify some proofs

* feat(order/filter/bases): define `filter.has_basis`

* Add `@[nolint]`

* +1 lemma, +1 simplified proof

* Remove whitespaces

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

* Ref. note nolint_ge

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

src/order/filter/bases.lean

@@ -0,0 +1,210 @@
+/-
+Copyright (c) 2020 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Yury Kudryashov
+-/
+
+import order.filter.basic
+
+/-! # Filter bases
+
+In this file we define `filter.has_basis l p s`, where `l` is a filter on `α`, `p` is a predicate
+on some index set `ι`, and `s : ι → set α`.
+
+## Main statements
+
+* `has_basis.mem_iff`, `has_basis.mem_of_superset`, `has_basis.mem_of_mem` : restate `t ∈ f` in terms
+  of a basis;
+* `basis_sets` : all sets of a filter form a basis;
+* `has_basis.inf`, `has_basis.inf_principal`, `has_basis.prod`, `has_basis.prod_self`,
+  `has_basis.map`, `has_basis.comap` : combinators to construct filters of `l ⊓ l'`,
+  `l ⊓ principal t`, `l.prod l'`, `l.prod l`, `l.map f`, `l.comap f` respectively;
+* `has_basis.le_iff`, `has_basis.ge_iff`, has_basis.le_basis_iff` : restate `l ≤ l'` in terms
+  of bases.
+* `has_basis.tendsto_right_iff`, `has_basis.tendsto_left_iff`, `has_basis.tendsto_iff` : restate
+  `tendsto f l l'` in terms of bases.
+
+## Implementation notes
+
+As with `Union`/`bUnion`/`sUnion`, there are three different approaches to filter bases:
+
+* `has_basis l s`, `s : set (set α)`;
+* `has_basis l s`, `s : ι → set α`;
+* `has_basis l p s`, `p : ι → Prop`, `s : ι → set α`.
+
+We use the latter one because, e.g., `𝓝 x` in an `emetric_space` or in a `metric_space` has a basis
+of this form. The other two can be emulated using `s = id` or `p = λ _, true`.
+
+With this approach sometimes one needs to `simp` the statement provided by the `has_basis`
+machinery, e.g., `simp only [exists_prop, true_and]` or `simp only [forall_const]` can help
+with the case `p = λ _, true`.
+-/
+
+namespace filter
+variables {α : Type*} {β : Type*} {γ : Type*} {ι : Type*} {ι' : Type*}
+
+open set lattice
+
+/-- We say that a filter `l` has a 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`. -/
+protected def has_basis (l : filter α) (p : ι → Prop) (s : ι → set α) : Prop :=
+∀ t : set α, t ∈ l ↔ ∃ i (hi : p i), s i ⊆ t
+
+section same_type
+
+variables {l l' : filter α} {p : ι → Prop} {s : ι → set α} {t : set α} {i : ι}
+  {p' : ι' → Prop} {s' : ι' → set α} {i' : ι'}
+
+/-- Definition of `has_basis` unfolded to make it useful for `rw` and `simp`. -/
+lemma has_basis.mem_iff (hl : l.has_basis p s) : t ∈ l ↔ ∃ i (hi : p i), s i ⊆ t :=
+hl t
+
+lemma has_basis.mem_of_superset (hl : l.has_basis p s) (hi : p i) (ht : s i ⊆ t) : t ∈ l :=
+(hl t).2 ⟨i, hi, ht⟩
+
+lemma has_basis.mem_of_mem (hl : l.has_basis p s) (hi : p i) : s i ∈ l :=
+hl.mem_of_superset hi $ subset.refl _
+
+lemma has_basis.forall_nonempty_iff_ne_bot (hl : l.has_basis p s) :
+  (∀ {i}, p i → (s i).nonempty) ↔ l ≠ ⊥ :=
+⟨λ H, forall_sets_nonempty_iff_ne_bot.1 $
+  λ s hs, let ⟨i, hi, his⟩ := (hl s).1 hs in (H hi).of_subset his,
+  λ H i hi, inhabited_of_mem_sets H (hl.mem_of_mem hi)⟩
+
+lemma basis_sets (l : filter α) : l.has_basis (λ s : set α, s ∈ l) id :=
+λ t, exists_sets_subset_iff.symm
+
+lemma at_top_basis [nonempty α] [semilattice_sup α] :
+  (@at_top α _).has_basis (λ _, true) Ici :=
+λ t, by simpa only [exists_prop, true_and] using @mem_at_top_sets α _ _ t
+
+lemma at_top_basis' [semilattice_sup α] (a : α) :
+  (@at_top α _).has_basis (λ x, a ≤ x) Ici :=
+λ t, (@at_top_basis α ⟨a⟩ _ t).trans
+  ⟨λ ⟨x, _, hx⟩, ⟨x ⊔ a, le_sup_right, λ y hy, hx (le_trans le_sup_left hy)⟩,
+    λ ⟨x, _, hx⟩, ⟨x, trivial, hx⟩⟩
+
+theorem has_basis.ge_iff (hl' : l'.has_basis p' s')  : l ≤ l' ↔ ∀ i', p' i' → s' i' ∈ l :=
+⟨λ h i' hi', h $ hl'.mem_of_mem hi',
+  λ h s hs, let ⟨i', hi', hs⟩ := (hl' s).1 hs in mem_sets_of_superset (h _ hi') hs⟩
+
+theorem has_basis.le_iff (hl : l.has_basis p s) : l ≤ l' ↔ ∀ t ∈ l', ∃ i (hi : p i), s i ⊆ t :=
+by simp only [le_def, hl.mem_iff]
+
+theorem has_basis.le_basis_iff (hl : l.has_basis p s) (hl' : l'.has_basis p' s') :
+  l ≤ l' ↔ ∀ i', p' i' → ∃ i (hi : p i), s i ⊆ s' i' :=
+by simp only [hl'.ge_iff, hl.mem_iff]
+
+lemma has_basis.inf (hl : l.has_basis p s) (hl' : l'.has_basis p' s') :
+  (l ⊓ l').has_basis (λ i : ι × ι', p i.1 ∧ p' i.2) (λ i, s i.1 ∩ s' i.2) :=
+begin
+  intro t,
+  simp only [mem_inf_sets, exists_prop, hl.mem_iff, hl'.mem_iff],
+  split,
+  { rintros ⟨t, ⟨i, hi, ht⟩, t', ⟨i', hi', ht'⟩, H⟩,
+    use [(i, i'), ⟨hi, hi'⟩, subset.trans (inter_subset_inter ht ht') H] },
+  { rintros ⟨⟨i, i'⟩, ⟨hi, hi'⟩, H⟩,
+    use [s i, i, hi, subset.refl _, s' i', i', hi', subset.refl _, H] }
+end
+
+lemma has_basis.inf_principal (hl : l.has_basis p s) (s' : set α) :
+  (l ⊓ principal s').has_basis p (λ i, s i ∩ s') :=
+λ t, by simp only [mem_inf_principal, hl.mem_iff, subset_def, mem_set_of_eq,
+  mem_inter_iff, and_imp]
+
+lemma has_basis.eq_binfi (h : l.has_basis p s) :
+  l = ⨅ i (_ : p i), principal (s i) :=
+eq_binfi_of_mem_sets_iff_exists_mem $ λ t, by simp only [h.mem_iff, mem_principal_sets]
+
+lemma has_basis.eq_infi (h : l.has_basis (λ _, true) s) :
+  l = ⨅ i, principal (s i) :=
+by simpa only [infi_true] using h.eq_binfi
+
+@[nolint] -- see Note [nolint_ge]
+lemma has_basis_infi_principal {s : ι → set α} (h : directed (≥) s) (ne : nonempty ι) :
+  (⨅ i, principal (s i)).has_basis (λ _, true) s :=
+begin
+  refine λ t, (mem_infi (h.mono_comp _ _) ne t).trans $
+    by simp only [exists_prop, true_and, mem_principal_sets],
+  exact λ _ _, principal_mono.2
+end
+
+@[nolint] -- see Note [nolint_ge]
+lemma has_basis_binfi_principal {s : β → set α} {S : set β} (h : directed_on (s ⁻¹'o (≥)) S)
+  (ne : S.nonempty) :
+  (⨅ i ∈ S, principal (s i)).has_basis (λ i, i ∈ S) s :=
+begin
+  refine λ t, (mem_binfi _ ne).trans $ by simp only [mem_principal_sets],
+  rw [directed_on_iff_directed, ← directed_comp, (∘)] at h ⊢,
+  apply h.mono_comp _ _,
+  exact λ _ _, principal_mono.2
+end
+
+lemma has_basis.map (f : α → β) (hl : l.has_basis p s) :
+  (l.map f).has_basis p (λ i, f '' (s i)) :=
+λ t, by simp only [mem_map, image_subset_iff, hl.mem_iff, preimage]
+
+lemma has_basis.comap (f : β → α) (hl : l.has_basis p s) :
+  (l.comap f).has_basis p (λ i, f ⁻¹' (s i)) :=
+begin
+  intro t,
+  simp only [mem_comap_sets, exists_prop, hl.mem_iff],
+  split,
+  { rintros ⟨t', ⟨i, hi, ht'⟩, H⟩,
+    exact ⟨i, hi, subset.trans (preimage_mono ht') H⟩ },
+  { rintros ⟨i, hi, H⟩,
+    exact ⟨s i, ⟨i, hi, subset.refl _⟩, H⟩ }
+end
+
+lemma has_basis.prod_self (hl : l.has_basis p s) :
+  (l.prod l).has_basis p (λ i, (s i).prod (s i)) :=
+begin
+  intro t,
+  apply mem_prod_iff.trans,
+  split,
+  { rintros ⟨t₁, ht₁, t₂, ht₂, H⟩,
+    rcases hl.mem_iff.1 (inter_mem_sets ht₁ ht₂) with ⟨i, hi, ht⟩,
+    exact ⟨i, hi, λ p ⟨hp₁, hp₂⟩, H ⟨(ht hp₁).1, (ht hp₂).2⟩⟩ },
+  { rintros ⟨i, hi, H⟩,
+    exact ⟨s i, hl.mem_of_mem hi, s i, hl.mem_of_mem hi, H⟩ }
+end
+
+end same_type
+
+section two_types
+
+variables {la : filter α} {pa : ι → Prop} {sa : ι → set α}
+  {lb : filter β} {pb : ι' → Prop} {sb : ι' → set β} {f : α → β}
+
+lemma has_basis.tendsto_left_iff (hla : la.has_basis pa sa) :
+  tendsto f la lb ↔ ∀ t ∈ lb, ∃ i (hi : pa i), ∀ x ∈ sa i, f x ∈ t :=
+by { simp only [tendsto, (hla.map f).le_iff, image_subset_iff], refl }
+
+lemma has_basis.tendsto_right_iff (hlb : lb.has_basis pb sb) :
+  tendsto f la lb ↔ ∀ i (hi : pb i), {x | f x ∈ sb i} ∈ la :=
+by simp only [tendsto, hlb.ge_iff, mem_map, preimage]
+
+lemma has_basis.tendsto_iff (hla : la.has_basis pa sa) (hlb : lb.has_basis pb sb) :
+  tendsto f la lb ↔ ∀ ib (hib : pb ib), ∃ ia (hia : pa ia), ∀ x ∈ sa ia, f x ∈ sb ib :=
+by simp only [hlb.tendsto_right_iff, hla.mem_iff, subset_def, mem_set_of_eq]
+
+lemma tendsto.basis_left (H : tendsto f la lb) (hla : la.has_basis pa sa) :
+  ∀ t ∈ lb, ∃ i (hi : pa i), ∀ x ∈ sa i, f x ∈ t :=
+hla.tendsto_left_iff.1 H
+
+lemma tendsto.basis_right (H : tendsto f la lb) (hlb : lb.has_basis pb sb) :
+  ∀ i (hi : pb i), {x | f x ∈ sb i} ∈ la :=
+hlb.tendsto_right_iff.1 H
+
+lemma tendsto.basis_both (H : tendsto f la lb) (hla : la.has_basis pa sa)
+  (hlb : lb.has_basis pb sb) :
+  ∀ ib (hib : pb ib), ∃ ia (hia : pa ia), ∀ x ∈ sa ia, f x ∈ sb ib :=
+(hla.tendsto_iff hlb).1 H
+
+lemma has_basis.prod (hla : la.has_basis pa sa) (hlb : lb.has_basis pb sb) :
+  (la.prod lb).has_basis (λ i : ι × ι', pa i.1 ∧ pb i.2) (λ i, (sa i.1).prod (sb i.2)) :=
+(hla.comap prod.fst).inf (hlb.comap prod.snd)
+
+end two_types
+
+end filter