theorem attains_min_on_closed_set_of_coercive {E : Type u} [NormedAddCommGroup E] [ProperSpace E] (f : E → EReal) {S : Set E} (hf : LowerSemicontinuous f) (hcoercive : IsCoerciveExtendedRealFunction f) (hS_closed : IsClosed S) (hS_dom : (S ∩ effective_domain f).Nonempty) : ∃ x ∈ S, IsMinOn f S x

Theorem 2.5: a proper closed coercive extended-real-valued function, equivalently here a lower semicontinuous coercive function, attains its minimum on every closed set S meeting its effective domain.