Zulip Chat Archive

Stream: Is there code for X?

Topic: A lemma about ultrafilters


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Oct 05 2020 at 14:24):

#4436


Last updated: May 17 2021 at 16:26 UTC