proposition: Lemma IVT (R : realType) (f : R -> R) (a b v : R) : a <= b -> {within `[a, b], continuous f} -> minr (f a) (f b) <= v <= maxr (f a) (f b) -> exists2 c, c \in `[a, b] & f c = v.
proof: Proof. move=> leab fcont; gen have ivt : f v fcont / f a <= v <= f b -> exists2 c, c \in `[a, b] & f c = v; last first. case: (leP (f a) (f b)) => [] _ fabv /=; first exact: ivt. have [| |c cab /oppr_inj] := ivt (- f) (- v); last by exists c. - by move=> x /=; apply/continuousN/fcont. - by rewrite lerNr opprK lerNr opprK andbC. move=> favfb; suff: is_interval (f @` `[a,b]). apply; last exact: favfb. - by exists a => //=; rewrite in_itv/= lexx. - by exists b => //=; rewrite in_itv/= leab lexx. apply/connected_intervalP/connected_continuous_connected => //. exact: segment_connected. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule