Library Interior

Require Import Utf8 Setoid.
Require Export Topology.
Require Import Notations Common.

Set Implicit Arguments.

Generalizable All Variables.


Local Open Scope topology_scope.

Section interior.
  Context `(T : Topology X).

The interior of a set contains all points which are in some open set contained in S

  Definition interior (S : Ensemble X) : Ensemble X :=
     (fun UU S Open U).

  Lemma interior_open S : Open (interior S).
    apply ArbitraryUnionOpen.

  Lemma interior_subset S : interior S S.
    repeat intro;
    destruct_head_hnf ArbitraryUnion;

  Lemma interior_open_same S : Open Sinterior S = S.
    intro H.
    apply Extensionality_Ensembles.
    split; repeat intro;
    destruct_head_hnf ArbitraryUnion;
    destruct_head_hnf and;

  Local Ltac t :=
    repeat (instantiate;
               || intro
               || assumption
               || (progress trivial)
               || (progress constructor)
               || (progress (etransitivity; eassumption); instantiate)
               || (progress destruct_head_hnf ArbitraryUnion)
               || (progress destruct_head_hnf and)
               || (progress destruct_head_hnf @Intersection)
               || (apply Intersection_Included_morr)
               || (apply FiniteIntersectionOpen)
               || (apply interior_open)
               || (progress firstorder))).

  Lemma interior_respect_subset U V : U Vinterior U interior V.
    match goal with
      | [ H0 : ?Xj ?U, H1 : Open ?Xj, H2 : ?x ?Xj
          |- ?x interior ?V ]
        ⇒ ( (Xj interior V))
      match goal with
        | _
          match goal with
            | [ H : _, H' : _ |- _ ] ⇒ rewrite H in H'; solve [ t ]
End interior.