Zulip Chat Archive

Stream: maths

Topic: filter.eventually


Patrick Massot (Apr 04 2020 at 15:50):

@Sebastien Gouezel and @Yury G. Kudryashov am I missing some file when I can't find

lemma filter.frequently_iff {α : Type*} {f : filter α} {P : α  Prop} :
  ( x in f, P x)   U  f,  x  U, P x

Patrick Massot (Apr 04 2020 at 15:52):

and friends like

lemma filter.inf_neq_bot_iff_frequently_left {α : Type*} {f g : filter α} :
  f  g     {U}, U  f   x in g, x  U

Patrick Massot (Apr 04 2020 at 16:10):

Maybe I'm missing part of the API. I wrote:

example {β : Type*} {F : filter β} (u :   β) :
(map u at_top)  F     U  F,  N,  n  N, u n  U :=
by simp_rw [inf_neq_bot_iff_frequently_right,
                           frequently_map,
                           frequently_at_top]

where I can find only the last rewriting lemma in mathlib currently.

Patrick Massot (Apr 05 2020 at 12:06):

@Sebastien Gouezel while you're here, could you also answer this thread of questions?

Sebastien Gouezel (Apr 05 2020 at 12:21):

The goal of the ∀ᶠ and ∃ᶠnotations is precisely to avoid ever writing U ∈ f. It works pretty well in most situations, but sometimes this is unavoidable. I don't think the interface between the two points of view is well developed, so I wouldn't be surprised if your lemmas were not there. Still, filter.frequently_iff is a crazy gap!

Patrick Massot (Apr 05 2020 at 12:25):

Ok, this is what I thought. I think we should have those lemmas, but try to avoid using them when possible.

Patrick Massot (Apr 05 2020 at 16:47):

See #2330.


Last updated: Dec 20 2023 at 11:08 UTC