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: May 19 2021 at 03:22 UTC