proposition: Theorem f12_is_inverse_g21 : forall y : R2, y[=]f12 (g21 y).
proof: Proof. intro. unfold f12 in |- *. cut (y[=]Lim (inj_Q_G_as_CauchySeq R2 y)). intro. apply eq_transitive_unfolded with (y := Lim (inj_Q_G_as_CauchySeq R2 y)). assumption. apply Lim_well_def. unfold inj_Q_G_as_CauchySeq in |- *. unfold image_G_as_CauchySeq12 in |- *. change ((Build_CauchySeq R2 (fun m : nat => inj_Q R2 (CS_seq Q_as_COrdField (G_as_CauchySeq R2 y) m)) (CS_seq_inj_Q_G R2 y) :R_COrdField R2)[=] Build_CauchySeq R2 (fun n : nat => inj_Q R2 (CS_seq Q_as_COrdField (G_as_CauchySeq R1 (g21 y)) n)) (image_Cauchy12 (g21 y))) in |- *. change ((Build_CauchySeq R2 (fun m : nat => inj_Q R2 (CS_seq Q_as_COrdField (G_as_CauchySeq R2 y) m)) (inj_Q_Cauchy R2 (G_as_CauchySeq R2 y)) :R_COrdField R2)[=] Build_CauchySeq R2 (fun n : nat => inj_Q R2 (CS_seq Q_as_COrdField (G_as_CauchySeq R1 (g21 y)) n)) (inj_Q_Cauchy R2 (G_as_CauchySeq R1 (g21 y)))) in |- *. apply inj_seq_well_def with (g := G_as_CauchySeq R2 y) (h := G_as_CauchySeq R1 (g21 y)). apply inj_Q_one_one with (IR := R1). change ((Build_CauchySeq R1 (fun m : nat => inj_Q R1 (G R2 y m)) (image_Cauchy21 y) :R_COrdField R1)[=] Build_CauchySeq R1 (fun n : nat => inj_Q R1 (G R1 (g21 y) n)) (CS_seq_inj_Q_G R1 (g21 y))) in |- *. change ((image_G_as_CauchySeq21 y:R_COrdField R1)[=] inj_Q_G_as_CauchySeq R1 (g21 y)) in |- *. apply Lim_one_one with (IR := R1). apply eq_transitive_unfolded with (y := g21 y). 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