Notation for `filter.principal`

Stream: maths

[Yury G. Kudryashov]

I've just noticed that s ∈ 𝒫 t ↔ t ∈ 𝓟 s.

[Yury G. Kudryashov]

One of Ps means set.powerset and the other means filter.principal.

[Yury G. Kudryashov]

The symbols look much more similar in my Emacs (Hack font) than in Firefox (don't know how to figure out which font is used).

[Patrick Massot]

Sure, this is not an accident...

[Yury G. Kudryashov]

Should we add a warning to the docstring of filter.principal?

[Johan Commelin]

They are dual right? Shouldn't one of them be upside down?

[Yury G. Kudryashov]

I was proving something about filter.lift' powerset f and at some moment I had both in my tactic status output.