proposition: Lemma contract_sup S : S !=set0 -> contract (ereal_sup S) = sup (contract @` S).
proof: Proof. move=> S0; apply/eqP; rewrite eq_le; apply/andP; split; last first. apply sup_le_ub. by case: S0 => x Sx; exists (contract x), x. move=> x [y Sy] <-{x}; rewrite le_contract; exact/ereal_sup_ub. rewrite leNgt; apply/negP. set supc := sup _; set csup := contract _; move=> ltsup. suff [y [ysupS ?]] : exists y, y < ereal_sup S /\ ubound S y. have : ereal_sup S <= y by apply ub_ereal_sup. by move/(lt_le_trans ysupS); rewrite ltxx. suff [x [? [ubSx x1]]] : exists x, (x < csup)%R /\ ubound (contract @` S) x /\ (`|x| <= 1)%R. exists (expand x); split => [|y Sy]. by rewrite -(contractK (ereal_sup S)) lt_expand // inE // contract_le1. by rewrite -(contractK y) le_expand //; apply ubSx; exists y. exists ((supc + csup) / 2); split; first by rewrite midf_lt. split => [r [y Sy <-{r}]|]. rewrite (@le_trans _ _ supc) ?midf_le //; last by rewrite ltW. apply sup_ub; last by exists y. by exists 1%R => r [z Sz <-]; case/ler_normlP : (contract_le1 z). rewrite ler_norml; apply/andP; split; last first. rewrite ler_pdivrMr // mul1r (_ : 2 = 1 + 1)%R // lerD //. by case/ler_normlP : (sup_contract_le1 S0). by case/ler_normlP : (contract_le1 (ereal_sup S)). rewrite ler_pdivlMr // (_ : 2 = 1 + 1)%R // mulN1r opprD lerD //. by case/ler_normlP : (sup_contract_le1 S0); rewrite lerNl. by case/ler_normlP : (contract_le1 (ereal_sup S)); rewrite lerNl. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(fsbigop cardinality set_interval) reals signed topology constructive_ereal