sInf S ∈ S

Stream: maths

[Martin Dvořák]

import Mathlib

example {T : Type} [ConditionallyCompleteLinearOrder T] {S : Set T}
    (hSn : Nonempty S) (hSb : BddBelow S) :
    sInf S ∈ S := by
  exact?

Am I missing an assumption?

[Yaël Dillies]

Yes, that the order is locally finite

[Martin Dvořák]

I probably shouldn't've used sInf in the first place.
I want to say that an affine map on a nonempty compact set has a minimum (and do something with it).
Which (noncomputable) function should I call to say "minimum" here?

[Yaël Dillies]

docs#Classical.choose ?

[Martin Dvořák]

I mean for the "minimum" part. My choice of sInf or iInf was probably wrong.

[Yaël Dillies]

I mean sInf/iInf is the correct function?

[Martin Dvořák]

Maybe docs#IsCompact.exists_isMinOn is what I need.

[Anatole Dedecker]

In your setup it’s probably easier to use docs#sInf and docs#IsCompact.sInf_mem. But note that docs#IsCompact.exists_isMinOn is mathematically stronger because it needs no completeness assumption on the ambient order, e.g it holds even for compact subsets of the rationals (which are quite rare, granted)