generalised eventually_at_top

Stream: Is there code for X?

[Bhavik Mehta]

example {f : ℝ → Prop} (h : ∀ᶠ x : ℝ in at_top, f x) (c' : ℝ) : ∃ c > c', ∀ y ≥ c, f y :=

If this were the other way round, I could use filter_upwards, but right now it seems like I need to do something manual with max and eventually_at_top. Is there a clean filter way of doing this?

[Yaël Dillies]

You forgot @[nolint no_or_gt] :upside_down:

[Bhavik Mehta]

Maybe a clearer way of saying what I want:

example {f : ℝ → Prop} (h : ∀ᶠ x : ℝ in at_top, f x) : ∃ c, ∀ y ≥ c, f y :=
eventually_at_top.1 h

example {f : ℝ → Prop} (h : ∀ᶠ x : ℝ in at_top, f x) : ∃ᶠ c in at_top, ∀ y ≥ c, f y :=
sorry

[Bhavik Mehta]

Yaël Dillies said:

You forgot @[nolint no_or_gt] :upside_down:

No, I didn't. Gt and ge are acceptable (and fairly common) in binders

[Bhavik Mehta]

For example, the lemma I want to generalise: docs#filter.eventually_at_top

[Yaël Dillies]

But we've decided to move away from them a few months ago.

[Bhavik Mehta]

Yaël Dillies said:

But we've decided to move away from them a few months ago.

The linter won't complain in this case though, which is why I didn't forget the nolint attribute

[Yaël Dillies]

I feel like what you're asking for is basically the definition of ∀ᶠ. I don't know the correct way to do with the API, but you can extract c directly from the definition of at_top as the filter infimum (so set supremum) of principal filters.

[Bhavik Mehta]

I think you're talking about docs#filter.eventually_at_top as "the definition", which does get me the value of c out, but as I mentioned this would then require a maximum or some other manual method to get the answer

[Bhavik Mehta]

It's certainly possible, but my question is if there's a cleaner way to get there!

[Yaël Dillies]

No, I'm talking about the literal definition. But indeed it sounds a bit ugly to dig in the def rather than use the API.

[Bhavik Mehta]

Here's a slight improvement on my original:

example {f : ℝ → Prop} (h : ∀ᶠ x : ℝ in at_top, f x) : ∃ᶠ c in at_top, ∀ y ≥ c, f y :=
begin
  rw frequently_at_top,
  intro a,
  exact (at_top_basis' a).mem_iff.1 h,
end

[Bhavik Mehta]

example {f : ℝ → Prop} (h : ∀ᶠ x : ℝ in at_top, f x) : ∀ c', ∃ c ≥ c', ∀ y ≥ c, f y :=
λ c', (at_top_basis' c').mem_iff.1 h

[Bhavik Mehta]

(at_top_basis' _).mem_iff works nicely in my case, but I'll leave this open in case others have other suggestions