filter.has_antitone_basis

Stream: maths

[Yury G. Kudryashov]

@Patrick Massot Do you ever need docs#filter.has_antitone_basis for p ≠ λ _, true? If not, what do you think about dropping the p argument?

[Yury G. Kudryashov]

I checked that p ≠ λ _, true is never needed in mathlib.

[Eric Wieser]

Can we use antitone in that definition?

[Patrick Massot]

I don't remember but if you checked then you can remove it. (Maybe you can check LTE as well but I would be very surprised).

[Yaël Dillies]

Eric Wieser said:

Can we use antitone in that definition?

If we remove p, yes. Else we'll need antitone_on.

[Yury G. Kudryashov]

I'm working on it (with no p and with antitone)