feat(topology/basic): add is_open_iff_ultrafilter (#4529)

Requested on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F)
by Adam Topaz

src/order/filter/ultrafilter.lean

@@ -211,11 +211,18 @@ begin
   exact absurd this u'.1
 end
 
+lemma le_iff_ultrafilter {l₁ l₂ : filter α} :
+  l₁ ≤ l₂ ↔ ∀ g, is_ultrafilter g → g ≤ l₁ → g ≤ l₂ :=
+by { rw [sup_of_ultrafilters l₁] { occs := occurrences.pos [1] }, simp only [supr_le_iff] }
+
+lemma mem_iff_ultrafilter {l : filter α} {s : set α} :
+  s ∈ l ↔ ∀ g, is_ultrafilter g → g ≤ l → s ∈ g :=
+by simpa only [← le_principal_iff] using le_iff_ultrafilter
+
 /-- The `tendsto` relation can be checked on ultrafilters. -/
 lemma tendsto_iff_ultrafilter (f : α → β) (l₁ : filter α) (l₂ : filter β) :
   tendsto f l₁ l₂ ↔ ∀ g, is_ultrafilter g → g ≤ l₁ → g.map f ≤ l₂ :=
-⟨assume h g u gx, le_trans (map_mono gx) h,
- assume h, by rw [sup_of_ultrafilters l₁]; simpa only [tendsto, map_supr, supr_le_iff]⟩
+tendsto_iff_comap.trans $ le_iff_ultrafilter.trans $ by simp only [map_le_iff_le_comap]
 
 /-- The ultrafilter monad. The monad structure on ultrafilters is the
   restriction of the one on filters. -/

src/topology/basic.lean

@@ -691,6 +691,10 @@ calc is_open s ↔ s ⊆ interior s : subset_interior_iff_open.symm
 lemma is_open_iff_mem_nhds {s : set α} : is_open s ↔ ∀a∈s, s ∈ 𝓝 a :=
 is_open_iff_nhds.trans $ forall_congr $ λ _, imp_congr_right $ λ _, le_principal_iff
 
+theorem is_open_iff_ultrafilter {s : set α} :
+  is_open s ↔ (∀ (x ∈ s) (l : filter α), is_ultrafilter l → l ≤ 𝓝 x → s ∈ l) :=
+by simp_rw [is_open_iff_mem_nhds, @mem_iff_ultrafilter _ (𝓝 _)]
+
 lemma mem_closure_iff_frequently {s : set α} {a : α} : a ∈ closure s ↔ ∃ᶠ x in 𝓝 a, x ∈ s :=
 by rw [filter.frequently, filter.eventually, ← mem_interior_iff_mem_nhds,
   closure_eq_compl_interior_compl]; refl