Filters in mathlib

Stream: new members

[Pedro Minicz]

Is there any particular reason why filter.has_top is {s : set α | ∀ (x : α), x ∈ s} and not {set.univ}. I strongly believe both are equivalent, except that the latter is clearer.

[Pedro Minicz]

Also, any reason why the preorder on filter is f ≤ g := g ⊆ f and not f ⊆ g?

[Yury G. Kudryashov]

Pedro Minicz said:

Is there any particular reason why filter.has_top is {s : set α | ∀ (x : α), x ∈ s} and not {set.univ}. I strongly believe both are equivalent, except that the latter is clearer.

This and some other definitions are optimized for better definitional equalities. E.g., for top with the current definition s \in \top can be applied to x to get x \in s.

[Yury G. Kudryashov]

Pedro Minicz said:

Also, any reason why the preorder on filter is f ≤ g := g ⊆ f and not f ⊆ g?

This way principal is monotone.