proposition: Lemma Urysohns_Lemma_function_1: forall x:X, ~ In U1 x -> Urysohns_Lemma_function x = 1.
proof: Proof. intros. apply Rle_antisym. { apply Urysohns_Lemma_function_range. } unfold Urysohns_Lemma_function. destruct inf as [y]. simpl. apply i. red. intros. destruct H0; [ | destruct H0; now right ]. destruct H0. destruct x0. destruct H0. assert (~ (m < (nat_of_P (pos_power2 n)))%nat). { intro. assert (forall n:nat, dr_eq (m_over_2_to_n (nat_of_P (pos_power2 n)) n) (m_over_2_to_n 1 0)). { induction n0. - simpl. unfold nat_of_P. simpl. apply dr_eq_refl. - apply dr_eq_trans with (2:=IHn0). apply dr_eq_sym. replace (nat_of_P (pos_power2 (S n0))) with ((2 * nat_of_P (pos_power2 n0))%nat). + apply dr_eq_scale. + simpl pos_power2. now rewrite Pos2Nat.inj_xO. } assert (dr_lt (m_over_2_to_n m n) (m_over_2_to_n 1 0)). { apply dr_lt_wd with (m_over_2_to_n m n) (m_over_2_to_n (nat_of_P (pos_power2 n)) n); trivial. - now apply intro_dr_lt. - apply dr_eq_refl. } pose proof (U_dyadic_incr _ _ H4). simpl (U_dyadic (m_over_2_to_n 1 0)) in H5. assert (Included (U_dyadic (m_over_2_to_n m n)) U1). { red. intros. now apply H5, closure_inflationary. } contradiction H. now apply H6. } assert ((m >= nat_of_P (pos_power2 n))%nat) by auto with zarith. red in H3. assert ((nat_of_P (pos_power2 n) < m \/ (nat_of_P (pos_power2 n) = m))%nat) by now apply Nat.lt_eq_cases. rewrite H1. replace 1 with (Q2R (dr2Q (m_over_2_to_n 1 0))). - match goal with |- ?a >= ?b => cut (b <= a); auto with real end. apply Qle_Rle. unfold dr2Q. unfold Qle. simpl. ring_simplify. rewrite Zpos_eq_Z_of_nat_o_nat_of_P. auto with zarith. - unfold Q2R. simpl. field. Qed.
imports: Coq(Reals Lia Lra ClassicalChoice) RationalsInReals TopologicalSpaces InteriorsClosures Div2 Even Arith RTopology