InvImage.v

Require Import Image.

Arguments Im {U V}.
Arguments In {U}.
Arguments Included {U}.

Section InvImage.

Variables U V : Type.

Inductive InvIm (Y : Ensemble V) (f : U -> V) : Ensemble U :=
  InvIm_intro : forall x : U, In Y (f x) -> In (InvIm Y f) x.

(* x ∈ f^(-1)(Y) <=> f(x) ∈ Y *)
Example inv_example_1 (Y:Ensemble V) (f:U -> V) (x:U) : 
  In (InvIm Y f) x <-> In Y (f x).
Proof.
  split.
  - (* -> *)
    intro x_in_InvImY.
    inversion x_in_InvImY as [y f_x_in_Y].
    assumption.
  - (* <- *)
    intro f_x_in_Y.
    apply (InvIm_intro Y f x f_x_in_Y).
Qed.

(* X ⊆ f^(-1)(Y) <=> f(X) ⊆ Y *)
Example inv_example_2 (X:Ensemble U) (Y:Ensemble V) (f:U -> V) : 
  Included X (InvIm Y f) <-> Included (Im X f) Y.
Proof.
  split.
  - (* -> *)
    intros X_included_InvImY y y_in_f_Y.
    assert (H := Im_inv U V X f y y_in_f_Y).
    inversion H.
    inversion H0 as [x_in_X f_x_eq_y].
    assert (x_in_InvImY := (X_included_InvImY x x_in_X)).
    rewrite <- f_x_eq_y.
    apply (inv_example_1 Y f x).
    assumption.
  - (* <- *)
    intros f_X_included_Y x x_in_X.
    assert (f_x_in_f_X := Im_intro U V X f x x_in_X (f x) eq_refl).
    assert (f_x_in_Y := f_X_included_Y (f x) f_x_in_f_X).
    apply (inv_example_1 Y f x).
    assumption.
Qed.

End InvImage.

MSpace.v

Require Import Ensembles.
Require Import Rlimit.
Require Import RIneq.
Require Import ZArith Psatz.
Require Import Image.
Require Import InvImage.

Arguments Im {U V}.
Arguments InvIm {U V}.
Arguments In {U}.
Arguments dist {m}.
Arguments Included {U}.
Arguments inv_example_1 {U V}.
Arguments inv_example_2 {U V}.

Open Scope R_scope.

Section MSpace.

Variable M_X : Metric_Space.
Variable M_Y : Metric_Space.

Definition N {M : Metric_Space} (a : Base M) (ε : posreal) : Ensemble (Base M) := fun r => dist a r < ε.

Example N_in {M : Metric_Space} (a : Base M) (ε : posreal) : 
  In (N a ε) a.
Proof.
  unfold In.
  unfold N.
  assert (a = a) by reflexivity.
  apply (dist_refl M a a) in H.
  rewrite H.
  apply cond_pos.
Qed.

Definition Od {M : Metric_Space} (U : Ensemble (Base M)) : Prop :=
  forall x, In U x ->
    exists ε:posreal,
      Included (N x ε) U.
(* Arguments Od M U /. *)
(* open set U:             *)
(* ∀x∈U, ∃ε>0, N(x; ε) ⊆ U *)

Definition posreal_to_R (ε : posreal) :=
  match ε with
  | {| pos := r |} => r
  end.

Ltac alias t v v0 name :=
  (assert (exists v:t, v = v0)
  as alias_H_name by (exists v0; reflexivity);
  inversion_clear alias_H_name as [v name]).

Example N_in_Od {M : Metric_Space} (a : Base M) ε : Od (N a ε).
Proof.
  intros x x_in_N_a_ε.
  unfold In in x_in_N_a_ε.
  unfold N in x_in_N_a_ε.
  alias posreal δ (mkposreal (ε - (dist a x)) (Rlt_Rminus (dist a x) ε x_in_N_a_ε)) δ_eq.
  exists δ.
  unfold Included.
  unfold In.
  unfold N.
  intros x' x'_in_N_x_δ.
  assert (δ + (dist a x + dist x x') = ε + dist x x') as δ_ε_eq.
  -
    rewrite <- (Rplus_assoc δ (dist a x) (dist x x')).
    assert (posreal_to_R δ + (dist a x) = ε) as posreal_to_eq.
    +
      rewrite δ_eq.
      compute.
      lra.
    +
      assert (pos δ = (posreal_to_R δ)) as pos_eq.
      *
        rewrite δ_eq.
        compute.
        lra.
      *
        rewrite <- pos_eq in posreal_to_eq.
        rewrite posreal_to_eq.
        reflexivity.
  -
    assert (dist_tri := dist_tri M a x' x).
    inversion dist_tri as [lt|eq].
    + (* lt *)
      assert (H1 := Rplus_lt_compat (dist x x') δ (dist a x') (dist a x + dist x x') x'_in_N_x_δ lt). 
      rewrite δ_ε_eq in H1.
      rewrite Rplus_comm in H1.
      apply Rplus_lt_reg_r in H1.
      assumption.
    + (* eq *)
      apply (Rplus_lt_compat_r (dist a x')) in x'_in_N_x_δ.
      replace (δ + dist a x')
        with (δ + (dist a x + dist x x'))
        in x'_in_N_x_δ by (rewrite eq; reflexivity).
      rewrite δ_ε_eq in x'_in_N_x_δ.
      rewrite Rplus_comm in x'_in_N_x_δ.
      apply Rplus_lt_reg_r in x'_in_N_x_δ.
      assumption.
Qed.

Definition Continuous_Map_Def (f : Base M_X -> Base M_Y) := 
  forall x:Base M_X,
    forall ε:posreal,
      exists δ:posreal,
        Included (Im (N x δ) f) (N (f x) ε).
Arguments Continuous_Map_Def / f.
(* continuous map f:                             *)
(* ∀x∈X, ∀ε>0, ∃δ>0, f(N_X(x; δ)) ⊆ N_Y(f(x); ε) *)

Definition Continuous_Map_Def_2 (f : Base M_X -> Base M_Y) := 
  forall U : Ensemble (Base M_Y),
    Od U -> Od (InvIm U f).
Arguments Continuous_Map_Def_2 / f.

Example CM_law_eq : forall f : Base M_X -> Base M_Y,
  Continuous_Map_Def f <-> Continuous_Map_Def_2 f.
Proof.
  intro f.
  simpl.
  split.
  - (* -> *)
    intros Continuous_Map_Def V V_in_Od a a_in_InvIm_f_V.
    apply (inv_example_1 V f a) in a_in_InvIm_f_V as f_a_in_V.
    unfold Od in V_in_Od.
    assert (V_Od_prop := V_in_Od (f a) f_a_in_V).
    inversion V_Od_prop as [ε V_Od_prop_].
    assert (suff := Continuous_Map_Def a ε).
    inversion_clear suff as [δ suff_].
    exists δ.
    apply (inv_example_2 (N a δ) V f).
    apply (Inclusion_is_transitive (Base M_Y) (Im (N a δ) f) (N (f a) ε) V suff_ V_Od_prop_).
(*   ∀V ∈ Od(Y)                                            *)
(*     a ∈ f^(-1)(V) <=> f(a) ∈ V                          *)
(*       ∃ε>0, N(f(a); ε) ⊆ V by Vは開集合 - (1)           *)
(*         ∃δ>0, f(N(x; δ)) ⊆ N(f(x); ε) by 十分条件 - (2) *)
(*           f(N(x; δ)) ⊆ V by (1), (2)                    *)
(*           N(x; δ) ⊆ f^(-1)(V)                           *)
(*           f^(-1)(V) ∈ Od(X)                             *)
  - (* <- *)
    intros Continuous_Map_Def_2 x ε.
    assert (N_f_x_ε_in_Od := N_in_Od (f x) ε).
    apply Continuous_Map_Def_2 in N_f_x_ε_in_Od.
    unfold Od in N_f_x_ε_in_Od.
    specialize N_f_x_ε_in_Od with (x0 := x).
    assert (In (N (f x) ε) (f x)) as f_x_in_N_f_x_ε by (apply N_in).
    apply inv_example_1 in f_x_in_N_f_x_ε.
    apply N_f_x_ε_in_Od in f_x_in_N_f_x_ε.
    inversion_clear f_x_in_N_f_x_ε as [δ H].
    exists δ.
    apply inv_example_2.
    assumption.
Qed.
(*   ∀x∈X, ∀ε>0                                            *)
(*     N(f(x); ε) ∈ Od(Y) by 近傍は開集合                  *)
(*     f^(-1)(N(f(x); ε)) ∈ Od(X) by 十分条件 - (1)        *)
(*     ∃δ>0, N(x; δ) ⊆ f^(-1)(N(f(x); ε)) by (1) - (2)     *)
(*     f(N(x; δ)) ⊆ N(f(x); ε) by (2)                      *)

End MSpace.