# Library Closure

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

Set Implicit Arguments.

Generalizable All Variables.

## Closure

Local Open Scope topology_scope.

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

The closure of a set is the intersection of all closed sets containing that set.

Definition closure (S : Ensemble X) : Ensemble X :=
(fun US U Closed U).

Lemma closure_closed S : Closed (closure S).
repeat unfold Closed, closure, ArbitraryIntersection.
rewrite complement_idempotent.
apply ArbitraryUnionOpen.
firstorder.
match goal with
| [ H : _ |- _ ] ⇒ rewrite complement_idempotent in H
end.
assumption.
Qed.

Lemma closure_superset S : S closure S.
repeat intro;
firstorder.
Qed.

Local Ltac t0 :=
repeat match goal with
| _eassumption
| _progress (repeat (split || intro))
| _progress (repeat unfold closure, ArbitraryIntersection, Closed, In in *; trivial)
| [ H : _ |- _ ] ⇒ rewrite complement_idempotent in H
| [ H : _ |- _ ] ⇒ hnf in H; rewrite complement_idempotent in H
| _apply Extensionality_Ensembles
| _progress (hnf; repeat rewrite complement_idempotent)
| _progress intuition
| _progress firstorder
end.

Local Ltac t1' tac := repeat ((progress t0) || (progress tac)).
Local Ltac t1'' tac :=
t1' tac;
try match goal with
| [ H : _ |- _ ] ⇒ apply H; solve [ t1' tac ]
end.
Local Ltac t1 tac :=
t1' tac;
match goal with
| _apply NNPP; solve [ t1'' tac ]
end.

Lemma closure_closed_same S : Closed Sclosure S = S.
t1 ltac:( (Complement X S)).
Qed.

Lemma closure_respect_subset U V : U Vclosure U closure V.
t1'' ltac:(eexists; [ | eassumption ]).
Qed.
End closure.