## Stream: maths

### Topic: Notation for filter.principal

#### Yury G. Kudryashov (Jul 29 2020 at 14:39):

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

#### Yury G. Kudryashov (Jul 29 2020 at 14:40):

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

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

#### Patrick Massot (Jul 29 2020 at 14:41):

Sure, this is not an accident...

#### Yury G. Kudryashov (Jul 29 2020 at 14:42):

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

#### Johan Commelin (Jul 29 2020 at 14:43):

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

#### 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