proposition: Lemma EVT_min (R : realType) (f : R -> R) (a b : R) : a <= b -> {within `[a, b], continuous f} -> exists2 c, c \in `[a, b]%R & forall t, t \in `[a, b]%R -> f c <= f t.
proof: Proof. move=> leab fcont. have /(EVT_max leab) [c clr fcmax] : {within `[a, b], continuous (- f)}. by move=> ?; apply: continuousN => ?; exact: fcont. by exists c => // ? /fcmax; rewrite lerN2. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum matrix interval) mathcomp(mathcomp_extra boolp classical_sets functions) reals signed topology prodnormedzmodule normedtype landau forms