proposition: Theorem g21_is_inverse_f12 : forall y : R1, y[=]g21 (f12 y).
proof: Proof. intro. unfold g21 in |- *. cut (y[=]Lim (inj_Q_G_as_CauchySeq R1 y)). intro. apply eq_transitive_unfolded with (y := Lim (inj_Q_G_as_CauchySeq R1 y)). assumption. apply Lim_well_def. unfold inj_Q_G_as_CauchySeq in |- *. unfold image_G_as_CauchySeq21 in |- *. change ((Build_CauchySeq R1 (fun m : nat => inj_Q R1 (CS_seq Q_as_COrdField (G_as_CauchySeq R1 y) m)) (CS_seq_inj_Q_G R1 y) :R_COrdField R1)[=] Build_CauchySeq R1 (fun n : nat => inj_Q R1 (CS_seq Q_as_COrdField (G_as_CauchySeq R2 (f12 y)) n)) (image_Cauchy21 (f12 y))) in |- *. change ((Build_CauchySeq R1 (fun m : nat => inj_Q R1 (CS_seq Q_as_COrdField (G_as_CauchySeq R1 y) m)) (inj_Q_Cauchy R1 (G_as_CauchySeq R1 y)) :R_COrdField R1)[=] Build_CauchySeq R1 (fun n : nat => inj_Q R1 (CS_seq Q_as_COrdField (G_as_CauchySeq R2 (f12 y)) n)) (inj_Q_Cauchy R1 (G_as_CauchySeq R2 (f12 y)))) in |- *. apply inj_seq_well_def with (g := G_as_CauchySeq R1 y) (h := G_as_CauchySeq R2 (f12 y)). apply inj_Q_one_one with (IR := R2). change ((image_G_as_CauchySeq12 y:R_COrdField R2)[=] inj_Q_G_as_CauchySeq R2 (f12 y)) in |- *. apply Lim_one_one with (IR := R2). apply eq_transitive_unfolded with (y := f12 y). change (f12 y[=]f12 y) in |- *. apply eq_reflexive_unfolded. apply SeqLimit_unique. apply x_is_SeqLimit_G. apply SeqLimit_unique. apply x_is_SeqLimit_G. Qed.
imports: CoRN.reals.Q_dense CoRN.reals.R_morphism