bdd_above/below_on

Stream: general

[Mantas Baksys]

Sorry, I may have been unclear here. What I mean by bdd_above_on is that a set is bdd_above + it has an upper bound, which belongs to a given set.

[Notification Bot]

Mantas Baksys has marked this topic as unresolved.

[Floris van Doorn]

That might be a useful notion to have. For the extreme value theorem, it is formulated like this: docs#is_compact.exists_forall_le.
I would call that something like attains_maximum_on or something.

[Floris van Doorn]

Oh wait, never mind. You don't have a function in your formulation. I think your notion is exists x, is_greatest s x. I'm not sure if it is useful to add a new notion for that.

[Mantas Baksys]

It would look something like ∃ (x : α), x ∈ t → is_greatest s x. If this is not useful to have on its own, then I presume I can pass this as a hypothesis in duplicating the content of order.bounds to monotone_on?

[Floris van Doorn]

oh, you have two sets s and t.
Perhaps you can just write (t ∩ upper_bounds s).nonempty or (t ∩ s ∩ upper_bounds s).nonempty, depending on which one you mean.

[Mantas Baksys]

I certainly can go with these! I meant the former, as I'm planning to work in the setup s ⊆ t, where monotone_on f t

[Yury G. Kudryashov]

We have docs#is_max_on