eventually eventually

Stream: Is there code for X?

[Heather Macbeth]

Can anyone suggest a more conceptual proof of the following lemma?

import order.filter.at_top_bot

open filter

variables {α : Type*} [semilattice_sup α] [nonempty α]

example {p : α × α → Prop} (hp : ∀ᶠ (x : α × α) in filter.at_top, p x) :
  ∀ᶠ k in at_top, ∀ᶠ l in at_top, p (k, l) :=
begin
  rw filter.eventually_at_top_prod_self at hp,
  obtain ⟨N, hN⟩ := hp,
  simp only [filter.eventually_at_top],
  use N,
  intros k hk,
  use N,
  intros l hl,
  exact hN k l hk hl,
end

[Heather Macbeth]

I was thinking it might be something about the relationship between the product and lexicographic orders, via some lemma like

example {p : α × α → Prop} (hp : ∀ᶠ (x : α × α) in filter.at_top, p x) :
  ∀ᶠ x in (@at_top (lex α α) _), p x :=
begin
  refine hp.filter_mono _,
  sorry -- `at_top ≤ at_top`
end

but I didn't get it working.

[Yaël Dillies]

The second lemma should be true indeed. Can't you first prove that a ≤ b in α × β implies a ≤ b in lex α β?

[Eric Wieser]

We should have such to_lex_mono lemmas for all the lex orders

[Heather Macbeth]

I'm asking in particular whether the first lemma can be deduced from the second!

[Yaël Dillies]

That's on my todo list!

[Yury G. Kudryashov]

Note that we have docs#filter.prod_at_top_at_top_eq and docs#filter.eventually.curry

[Heather Macbeth]

Perfect. Thank you @Yury G. Kudryashov!

[Yury G. Kudryashov]

AFAIR, I added filter.eventually.curry to get a similar lemma about nhds.

[Heather Macbeth]

Yes, that's my use case too (a fact about Cauchy sequences)

[Heather Macbeth]

here (which I will rename to mention curry)