proposition: Lemma Urysohns_Lemma_function_range: forall x:X, 0 <= Urysohns_Lemma_function x <= 1.
proof: Proof. intros. unfold Urysohns_Lemma_function. destruct inf as [y]. simpl. split. - apply i. red; intros. destruct H. + destruct H. rewrite H0. replace 0 with (Q2R 0) by lra. cut (Q2R 0 <= Q2R (dr2Q x0)); auto with real. apply Qle_Rle. destruct x0. unfold dr2Q, Qle. simpl. auto with zarith. + destruct H. auto with real. - cut (1 >= y); auto with real. apply i. right. constructor. Qed.
imports: Coq(Reals Lia Lra ClassicalChoice) RationalsInReals TopologicalSpaces InteriorsClosures Div2 Even Arith RTopology