Require Import Classical.

Definition B := nat -> nat.

Definition Top := B -> Prop.

Definition inclusion (X Y : Top) := forall z : B, X z -> Y z.
Definition equal (X Y : Top) := inclusion X Y /\ inclusion Y X.
Definition complement (X : Top) (z : B) := ~ X z.
Definition union (X Y : Top) (z : B) := X z \/ Y z.
Definition inter (X Y : Top) (z : B) := X z /\ Y z.

Definition neighbour (f : B) (n : nat) (g : B) :=
  forall m : nat, m <= n -> f m = g m.
Definition open (X : Top) :=
  forall f : B, X f -> exists n : nat, inclusion (neighbour f n) X.
Definition closed (X : Top) := open (complement X).
Definition dense (X : Top) :=
  forall (f : B) (n : nat), exists g : B, X g /\ neighbour f n g.
Definition closure (X : Top) (f : B) :=
  forall n : nat, exists g : B, X g /\ neighbour f n g.

Lemma refl_neighbour : forall (n : nat) (x : B), neighbour x n x.
unfold neighbour in |- *; auto with v62.
Qed.
Hint Resolve refl_neighbour.

Lemma trans_neighbour :
 forall (n : nat) (f g h : B),
 neighbour f n g -> neighbour g n h -> neighbour f n h.
unfold neighbour in |- *.
intros.
rewrite (H m); trivial with v62.
apply H0; trivial with v62.
Qed.

Lemma closedc_clX : forall X : Top, closed (closure X).
unfold closed, closure in |- *.
unfold open, complement in |- *.
intros X f complement_clX.
generalize
 (not_all_ex_not nat (fun n : nat => exists g : B, X g /\ neighbour f n g)
    complement_clX).
simple induction 1; intros n H1.
exists n.
unfold inclusion in |- *; intros g fng.
unfold not in |- *; intro H2.
apply H1.
elim (H2 n).
simple induction 1; intros.
exists x; split; trivial with v62.
apply trans_neighbour with g; trivial with v62.
Qed.
Hint Resolve closedc_clX.

Lemma Xinc_clX : forall X : Top, inclusion X (closure X).
unfold inclusion in |- *; intros X f Xf.
unfold closure in |- *; intro n.
exists f; split; trivial with v62.
Qed.

Lemma Lemma1 :
 forall X : Top,
 equal X (inter (closure X) (union X (complement (closure X)))).
unfold equal, inclusion in |- *; intro X; split.
unfold inter, union, closure in |- *; intros.
split.
intro n; exists z; split; auto with v62.
left; trivial with v62.
unfold inter, union, closure in |- *; intros.
elim H; intros.
elim H1; trivial with v62.
unfold complement in |- *; intros.
elim (H2 H0).
Qed.

Lemma density : forall X : Top, dense (union X (complement (closure X))).
unfold dense in |- *; intros X f n.
elim (classic (closure X f)).
intro clXf.
elim (clXf n).
simple induction 1.
intros; exists x.
split; trivial with v62.
unfold union in |- *.
left; trivial with v62.
intro notclXf.
exists f; intros.
split; trivial with v62.
unfold union in |- *.
right; trivial with v62.
Qed.
Hint Resolve density.

Theorem Rem :
 forall X : Top,
 exists Y : Top, (exists Z : Top, closed Y /\ dense Z /\ equal X (inter Y Z)).
intro X; exists (closure X).
exists (union X (complement (closure X))).
split; auto with v62.
split; auto with v62.
apply Lemma1.
Qed.
Require Import Lt.

Definition nbh := neighbour.
Definition clopen (X : Top) := open X /\ closed X.

Lemma clopenbasis : forall (f : B) (n : nat), clopen (nbh f n).
intros f n.
unfold clopen in |- *.
split.
unfold open in |- *; intro g.
intro Ofng.
exists (S n).
unfold inclusion in |- *.
intros h OhSnz.
unfold nbh in |- *; unfold neighbour in |- *.
intros m lemn.
unfold neighbour in OhSnz.
unfold nbh in Ofng; unfold neighbour in Ofng.
generalize (Ofng m lemn).
intro E; rewrite E.
auto with v62.
unfold closed, nbh in |- *.
unfold open, complement, neighbour in |- *.
intro g.
intro notgfn.
exists n.
unfold inclusion in |- *.
intro h.
intro hgn.
unfold not in |- *; intros fhn.
apply notgfn.
intros p psn.
rewrite (fhn p psn).
rewrite (hgn p psn); trivial with v62.
Qed.