proposition: Lemma Urysohns_Lemma_function_0: forall x:X, In U0 x -> Urysohns_Lemma_function x = 0.
proof: Proof. intros. apply Rle_antisym; [ | apply Urysohns_Lemma_function_range ]. unfold Urysohns_Lemma_function. destruct inf as [y]. simpl. cut (0 >= y); auto with real. apply i. left. exists (m_over_2_to_n 0 0). - now constructor. - unfold Q2R. simpl. ring. Qed.
imports: Coq(Reals Lia Lra ClassicalChoice) RationalsInReals TopologicalSpaces InteriorsClosures Div2 Even Arith RTopology