Finite version of IsCompact.exists_forall_le'

Stream: Is there code for X?

[Anatole Dedecker]

Do we have no Set.Finite version of docs#IsCompact.exists_forall_le' (the key part is I want no Nonempty assumption) ?

[Michael Rothgang]

Does #9872 help?

[Michael Rothgang]

AIUI, that should work for any compact set (with a ClosedIicTopology and a NoMaxOrder).

[Michael Rothgang]

Otherwise, I presume you can mimick that proof :-)

[Anatole Dedecker]

Well, this is the exact theorem I linked to indeed x) My point is that in the finite setting we don't want to have to introduce a topology to apply this lemma (even though mathematically it works perfectly fine)

[Michael Rothgang]

Sorry, I didn't check your link :face_palm:

[Michael Rothgang]

Well, I guess we don't have it. When submitting #9872, I checked and found no other result with a non-emptiness assumption.

[Michael Rothgang]

(deleted)

[Yaël Dillies]

So you want a purely order theoretical lemma?

[Yaël Dillies]

Cant' you make do with docs#Finset.exists_le ?

[Anatole Dedecker]

Okay let’s un-xy. Here and there when dealing with infimums of metrizable topologies (e.g around docs#WithSeminorms, or in #10678) you are given some finite set of positive real numbers, not necessarily nonempty, and you want to pick some epsilon less than all of these and still positive. Of course there are multiple ways around this, but I haven't found anything fully satisfactory yet.