feat(order/filter/countable_Inter): sup and inf (#3154)

src/order/filter/countable_Inter.lean

@@ -63,3 +63,27 @@ by { rw ← principal_empty, apply countable_Inter_filter_principal }
 
 instance countable_Inter_filter_top : countable_Inter_filter (⊤ : filter α) :=
 by { rw ← principal_univ, apply countable_Inter_filter_principal }
+
+/-- Infimum of two `countable_Inter_filter`s is a `countable_Inter_filter`. This is useful, e.g.,
+to automatically get an instance for `residual α ⊓ principal s`. -/
+instance countable_Inter_filter_inf (l₁ l₂ : filter α) [countable_Inter_filter l₁]
+  [countable_Inter_filter l₂] :
+  countable_Inter_filter (l₁ ⊓ l₂) :=
+begin
+  refine ⟨λ S hSc hS, _⟩,
+  choose s hs t ht hst using hS,
+  replace hs : (⋂ i ∈ S, s i ‹_›) ∈ l₁ := (countable_bInter_mem_sets hSc).2 hs,
+  replace ht : (⋂ i ∈ S, t i ‹_›) ∈ l₂ := (countable_bInter_mem_sets hSc).2 ht,
+  refine mem_sets_of_superset (inter_mem_inf_sets hs ht) (subset_sInter $ λ i hi, _),
+  refine subset.trans (inter_subset_inter _ _) (hst i hi);
+    exact Inter_subset_of_subset i (Inter_subset _ _)
+end
+
+/-- Supremum of two `countable_Inter_filter`s is a `countable_Inter_filter`. -/
+instance countable_Inter_filter_sup (l₁ l₂ : filter α) [countable_Inter_filter l₁]
+  [countable_Inter_filter l₂] :
+  countable_Inter_filter (l₁ ⊔ l₂) :=
+begin
+  refine ⟨λ S hSc hS, ⟨_, _⟩⟩; refine (countable_sInter_mem_sets hSc).2 (λ s hs, _),
+  exacts [(hS s hs).1, (hS s hs).2]
+end