Require Export TopologicalSpaces.
Require Export Ensembles.
Require Import EnsemblesImplicit.
Require Export InteriorsClosures.

Definition open_neighborhood {X:TopologicalSpace}
  (U:Ensemble (point_set X)) (x:point_set X) :=
  open U ∧ In U x.

Definition neighborhood {X:TopologicalSpace}
  (N:Ensemble (point_set X)) (x:point_set X) :=
  ∃ U:Ensemble (point_set X),
    open_neighborhood U x ∧ Included U N.

Lemma open_neighborhood_is_neighborhood: ∀ {X:TopologicalSpace}
  (U:Ensemble (point_set X)) (x:point_set X),
  open_neighborhood U x → neighborhood U x.
Proof.
intros.
∃ U; auto with sets.
Qed.

Lemma neighborhood_interior: ∀ {X:TopologicalSpace}
  (N:Ensemble (point_set X)) (x:point_set X),
  neighborhood N x → In (interior N) x.
Proof.
intros.
destruct H.
destruct H.
destruct H.
assert (Included x0 (interior N)).
apply interior_maximal; trivial.
auto with sets.
Qed.

Lemma interior_neighborhood: ∀ {X:TopologicalSpace}
  (N:Ensemble (point_set X)) (x:point_set X),
  In (interior N) x → neighborhood N x.
Proof.
intros.
∃ (interior N).
repeat split.
apply interior_open.
assumption.
apply interior_deflationary.
Qed.