## Stream: Is there code for X?

### Topic: A lemma about ultrafilters

#### Adam Topaz (Oct 05 2020 at 02:17):

Does mathlib have the following variant of exists_ultrafilter? I couldn't find anything similar.

lemma exists_ultrafilter' (S : set (set α)) (cond : ∀ T : finset (set α),
↑T ⊆ S → ⋂₀ (↑T : set (set α)) ≠ ∅) : ∃ F : filter α, S ⊆ F.sets ∧ is_ultrafilter F := sorry


#### Adam Topaz (Oct 05 2020 at 02:22):

If not, I could open a PR for this:
https://github.com/leanprover-community/mathlib/blob/b85798964d03672dc8c3123ccdd5a7fa2916f2eb/src/order/filter/ultrafilter.lean#L145

#### Adam Topaz (Oct 05 2020 at 14:24):

#4436

Last updated: May 17 2021 at 16:26 UTC