filter.eventually

Stream: maths

[Patrick Massot]

@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]

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]

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]

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

[Sebastien Gouezel]

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]

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

[Patrick Massot]

See #2330.