Eventually vacuously true statements

Stream: Is there code for X?

[Ryan Lahfa]

Is there nice ways to lift $(\forall x, \lnot p x) \implies (\forall x, p x \to q x)$ for any $p, q$ propositions for eventually filters, MWE:

import analysis.specific_limits

open filter

lemma eventually_false_of_not {α} {p q: α → Prop} {l: filter α}:
  (∀ᶠ x in l, ¬ p x) → (∀ᶠ x in l, p x → q x) := sorry

I think I can do it by brute-forcing stuff, mostly by proving that { x | p x } \notin l as { x | not(p(x)) } \in l (otherwise, intersection would be empty, and the empty set would be in the filter),

Therefore, { x | p x → q x } = univ, which should complete the proof. But I'm looking for more idiomatic ways to perform this proof rather than spamming definitions.

[Anatole Dedecker]

You can use docs#filter.eventually.mono and then you just have to give the pointwise proof

[Ryan Lahfa]

Anatole Dedecker said:

You can use docs#filter.eventually.mono and then you just have to give the pointwise proof

You're definitely super hacka :-)

[Ryan Lahfa]

For completeness:

lemma eventually_false_of_not {α} {p q: α → Prop} {l: filter α}
  (hnp: ∀ᶠ x in l, ¬ p x): (∀ᶠ x in l, p x → q x) :=
  eventually.mono hnp (λ x hnpx hpx, absurd hpx hnpx)