working with filter bases

Stream: general

[Bernd Losert]

So I have a filter expression of the form:

g⁻¹ • filter.map m ↑h ⊓ map n f

I need to show that this filter is not ne_bot. I would like to prove this using filter bases, but it is not clear to me how to get a filter bases for this kind of filter expression easily. Any tips?

[Anatole Dedecker]

Do you really mean "not ne_bot" or is it a typo ?

[Bernd Losert]

Oops. That was a typo. I meant I need to prove ne_bot.

[Filippo A. E. Nuccio]

Can you perhaps add a #mwe ?

[Anatole Dedecker]

Oh sorry I wanted to answer but I forgot. Does docs#filter.has_basis.inf_ne_bot_iff help you ? I say that's easier than explicitely constructing the filter basis just to show that is does not contain $\varnothing$

[Bernd Losert]

filter.has_basis.inf_ne_bot_iff is great, but I need one for the whole of g⁻¹ • filter.map m ↑h ⊓ map n f. I guess I can compose some of has_basis lemmas to get one for this whole expression. I will have to experiment. Thanks.