Zulip Chat Archive

Stream: maths

Topic: Notation for `filter.principal`


view this post on Zulip Yury G. Kudryashov (Jul 29 2020 at 14:39):

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

view this post on Zulip Yury G. Kudryashov (Jul 29 2020 at 14:40):

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

view this post on Zulip Yury G. Kudryashov (Jul 29 2020 at 14:41):

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).

view this post on Zulip Patrick Massot (Jul 29 2020 at 14:41):

Sure, this is not an accident...

view this post on Zulip Yury G. Kudryashov (Jul 29 2020 at 14:42):

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

view this post on Zulip Johan Commelin (Jul 29 2020 at 14:43):

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

view this post on Zulip Yury G. Kudryashov (Jul 29 2020 at 14:45):

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


Last updated: May 14 2021 at 18:28 UTC