proposition: Lemma urysohn_ext_itv A B x y : closed A -> closed B -> A `&` B = set0 -> x < y -> exists f : X -> R, [/\ continuous f, f @` A `<=` [set x], f @` B `<=` [set y] & range f `<=` `[x, y]].
proof: Proof. move=> cA cB A0 xy; move/normal_separatorP : normalX => urysohn_ext. have /(@uniform_separatorP _ R)[f [cf f01 f0 f1]] := urysohn_ext _ _ cA cB A0. pose g : X -> R := line_path x y \o f; exists g; split; rewrite /g /=. move=> t; apply: continuous_comp; first exact: cf. apply: (@continuousD R R^o). apply: continuousM; last exact: cvg_cst. by apply: (@continuousB R R^o) => //; exact: cvg_cst. by apply: continuousM; [exact: cvg_id|exact: cvg_cst]. - by rewrite -image_comp => z /= [? /f0 -> <-]; rewrite line_path0. - by rewrite -image_comp => z /= [? /f1 -> <-]; rewrite line_path1. - rewrite -image_comp; apply: (subset_trans (image_subset _ f01)). by rewrite range_line_path. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets fsbigop) mathcomp(functions cardinality set_interval) signed reals ereal topology normedtype sequences