atTop and atBot filters

Stream: mathlib4

[Yury G. Kudryashov]

In #23585, @Aaron Liu adds new filters atMax and atMin. What do you think about replacing the current atTop and atBot with these new filters?

[Yury G. Kudryashov]

Membership in atMax (which may replace atTop) is given by

theorem mem_atMax [Preorder α] (s : Set α) : s ∈ atMax ↔ ∀ x, ∃ y ≥ x, Ici y ⊆ s := Iff.rfl

[Yury G. Kudryashov]

For a directed order, the new filter is the same as atTop, so the only possible change is addition/removal of "directed" assumptions here and there.

[Sébastien Gouëzel]

Do you mean, we should change the definition of atTop with this new definition, to make it work also on non-directed orders, or we should have both and swap most theorems to use atMax instead of atTop? I would be fine with the first option (dropping some directedness assumptions in some lemmas would always be good) , but not with the second (too much disruption for a too small gain).

[Yaël Dillies]

Is this the correct filter for things happening "at all maximal elements"? What's Aaron's motivation for this filter?

[Aaron Liu]

My motivation is to have a useful notion of the "limit at infinity" in a non-directed order (for which atTop = ⊥). After thinking about it for a while this is the definition I came up with. So far I have proved

instance [Nonempty α] : NeBot (atMax : Filter α)

theorem atTop_le_atMax : (atTop : Filter α) ≤ atMax

theorem atMax_eq_atTop [IsDirected α (· ≤ ·)] : (atMax : Filter α) = atTop

theorem pure_le_atMax : pure x ≤ atMax ↔ IsMax x

and their duals, which are in the PR.

[Yury G. Kudryashov]

Sébastien Gouëzel said:

Do you mean, we should change the definition of atTop with this new definition, to make it work also on non-directed orders, or we should have both and swap most theorems to use atMax instead of atTop? I would be fine with the first option (dropping some directedness assumptions in some lemmas would always be good) , but not with the second (too much disruption for a too small gain).

This will drop directedness assumptions in some lemmas but add them in other lemmas. E.g., tendsto_atTop will require directedness with this new proof.

[Yury G. Kudryashov]

@Aaron Liu Do you have any specific types with non-directed orders where you care about atMax, or is it a theoretical exercise?

[Sébastien Gouëzel]

Yury G. Kudryashov said:

This will drop directedness assumptions in some lemmas but add them in other lemmas. E.g., tendsto_atTop will require directedness with this new proof.

Then I would need a convincing example to show me that the new definition is better than the current one.

[Aaron Liu]

Yury G. Kudryashov said:

Aaron Liu Do you have any specific types with non-directed orders where you care about atMax, or is it a theoretical exercise?

Mostly this is a theoretical exercise, but I recently found a place to to use this.

[Yury G. Kudryashov]

Any details?