Filter.EventuallyLT

Stream: Is there code for X?

[Yongxi Lin (Aaron)]

Does it map sense to have Filter.EventuallyLT and introduce the notation <ᶠ[ ]? I personally think APIs related to this will be useful because for example I can express that a function is μ almost everywhere positive by writing 0 <ᵐ[μ] fin lean.

[Aaron Liu]

we have docs#Filter.EventuallyEq and docs#Filter.EventuallyLE

[Aaron Liu]

but I don't see LT for some reason

[Aaron Liu]

probably makes sense to add it

[Yaël Dillies]

I think it would be quite confusing for f < g to not imply f <ᶠ[l] g!

[Yongxi Lin (Aaron)]

So I guess the confusion arises because we have two possible interpretations of f < g when f and g are two functions. The first one is pointwise strict inequality: ∀ x, f x < g x. The second one is ∀ x, f x ≤ g x and ∃ x, f x < g x(Pi.lt_def).

[Floris van Doorn]

Yaël Dillies said:

I think it would be quite confusing for f < g to not imply f <ᶠ[l] g!

It is also confusing that f < g doesn't imply f x < g x. I don't think adding this notation makes the situation worse, and I think would be nice to add.