# Library Topology.Nets

Require Export TopologicalSpaces.
Require Export DirectedSets.
Require Export InteriorsClosures.
Require Export Continuity.

Section Net.

Variable I:DirectedSet.
Variable X:TopologicalSpace.

Definition Net := DS_set Ipoint_set X.

Definition net_limit (x:Net) (x0:point_set X) : Prop :=
U:Ensemble (point_set X), open UIn U x0
for large i:DS_set I, In U (x i).

Definition net_cluster_point (x:Net) (x0:point_set X) : Prop :=
U:Ensemble (point_set X), open UIn U x0
arbitrarily large i:DS_set I, In U (x i).

Lemma net_limit_is_cluster_point: (x:Net) (x0:point_set X),
net_limit x x0net_cluster_point x x0.
Proof.
intros.
red; intros.
red; intros.
pose proof (H U H0 H1).
destruct H2.
destruct (DS_join_cond i x1).
destruct H3.
x2; split; trivial.
apply H2; trivial.
Qed.

Lemma net_limit_in_closure: (S:Ensemble (point_set X))
(x:Net) (x0:point_set X),
( arbitrarily large i:DS_set I, In S (x i)) →
net_limit x x0In (closure S) x0.
Proof.
intros.
apply NNPP.
red; intro.
pose proof (H0 (Complement (closure S))).
match type of H2 with | ?A → ?B → ?Cassert (C) end.
apply H2.
apply closure_closed.
assumption.
destruct H3.
pose proof (H x1).
destruct H4.
tauto.
apply closure_inflationary; tauto.
Qed.

Lemma net_cluster_point_in_closure: (S:Ensemble (point_set X))
(x:Net) (x0:point_set X),
(for large i:DS_set I, In S (x i)) →
net_cluster_point x x0In (closure S) x0.
Proof.
intros.
apply NNPP.
red; intro.
pose proof (H0 (Complement (closure S))).
match type of H2 with | ?A → ?B → ?Cassert (C) end.
apply H2.
apply closure_closed.
assumption.
destruct H.
destruct (H3 x1).
destruct H4.
apply closure_inflationary.
apply H; trivial.
Qed.

End Net.

Implicit Arguments net_limit [[I] [X]].
Implicit Arguments net_cluster_point [[I] [X]].
Implicit Arguments net_limit_is_cluster_point [[I] [X]].
Implicit Arguments net_limit_in_closure [[I] [X]].
Implicit Arguments net_cluster_point_in_closure [[I] [X]].

Section neighborhood_net.

Variable X:TopologicalSpace.
Variable x:point_set X.

Inductive neighborhood_net_DS_set : Type :=
| intro_neighborhood_net_DS :
(U:Ensemble (point_set X)) (y:point_set X),
open UIn U xIn U yneighborhood_net_DS_set.

Definition neighborhood_net_DS_ord
(Uy Vz:neighborhood_net_DS_set) : Prop :=
match Uy, Vz with
| intro_neighborhood_net_DS U _ _ _ _,
intro_neighborhood_net_DS V _ _ _ _
Included V U
end.

Definition neighborhood_net_DS : DirectedSet.
refine (Build_DirectedSet neighborhood_net_DS_set
neighborhood_net_DS_ord _ _).
constructor.
red; intros.
destruct x0.
simpl; auto with sets.
red; intros.
destruct x0; destruct y; destruct z.
simpl in H; simpl in H0; simpl.
auto with sets.

intros.
destruct i; destruct j.
assert (open (Intersection U U0)).
apply open_intersection2; trivial.
assert (In (Intersection U U0) x); auto with sets.

(intro_neighborhood_net_DS (Intersection U U0) x
H H0 H0).
simpl; auto with sets.
Defined.

Definition neighborhood_net : Net neighborhood_net_DS X :=
fun (x:neighborhood_net_DS_set) ⇒ match x with
| intro_neighborhood_net_DS _ y _ _ _y
end.

Lemma neighborhood_net_limit: net_limit neighborhood_net x.
Proof.
red; intros.
(intro_neighborhood_net_DS U x H H0 H0).
intros.
destruct j.
simpl in H1.
simpl.
auto with sets.
Qed.

End neighborhood_net.

Lemma net_limits_determine_topology:
{X:TopologicalSpace} (S:Ensemble (point_set X))
(x0:point_set X), In (closure S) x0
I:DirectedSet, x:Net I X,
( i:DS_set I, In S (x i)) net_limit x x0.
Proof.
intros.
assert ( U:Ensemble (point_set X), open UIn U x0
Inhabited (Intersection S U)).
intros.
apply NNPP; red; intro.
assert (Included (closure S) (Complement U)).
apply closure_minimal.
red; rewrite Complement_Complement; assumption.
red; intros.
red; red; red; intros.
x; auto with sets.
apply H3.
assumption.
pose (Ssel := fun n:neighborhood_net_DS_set X x0
match n with
| intro_neighborhood_net_DS V y _ _ _ ⇒ (In S y)
end).
pose (our_DS_set := {n:neighborhood_net_DS_set X x0 | Ssel n}).
pose (our_DS_ord := fun (n1 n2:our_DS_set) ⇒
neighborhood_net_DS_ord X x0 (proj1_sig n1) (proj1_sig n2)).
assert (preorder our_DS_ord).
constructor; red.
intros; red.
apply preord_refl.
apply (@DS_ord_cond (neighborhood_net_DS X x0)).
intros x y z.
unfold our_DS_ord; apply preord_trans.
apply (@DS_ord_cond (neighborhood_net_DS X x0)).
assert ( i j:our_DS_set, k:our_DS_set,
our_DS_ord i k our_DS_ord j k).
destruct i.
destruct x.
destruct j.
destruct x.
assert (open (Intersection U U0)).
apply open_intersection2; trivial.
assert (In (Intersection U U0) x0).
auto with sets.
assert (Inhabited (Intersection S (Intersection U U0))).
apply H0; trivial.
destruct H4.
destruct H4.
pose (k0 := intro_neighborhood_net_DS X x0
(Intersection U U0) x H2 H3 H5).
assert (Ssel k0).
red; unfold k0; simpl.
assumption.
(exist _ k0 H6).
split; red; simpl; auto with sets.

pose (our_DS := Build_DirectedSet our_DS_set our_DS_ord H1 H2).
our_DS.
(fun i:our_DS_setneighborhood_net X x0 (proj1_sig i)).
split.
intros.
destruct i.
destruct x.
simpl.
simpl in s.
assumption.

red; intros.
assert (Inhabited (Intersection S U)).
apply H0; trivial.
destruct H5.
destruct H5.
pose (i0 := intro_neighborhood_net_DS X x0
U x H3 H4 H6).
assert (Ssel i0).
simpl; assumption.
(exist _ i0 H7).
intros.
destruct j.
destruct x1.
simpl in H8.
red in H8; simpl in H8.
simpl.
auto with sets.
Qed.

Section Nets_and_continuity.

Variable X Y:TopologicalSpace.
Variable f:point_set Xpoint_set Y.

Lemma continuous_func_preserves_net_limits:
{I:DirectedSet} (x:Net I X) (x0:point_set X),
net_limit x x0continuous_at f x0
net_limit (fun i:DS_set If (x i)) (f x0).
Proof.
intros.
red; intros V ? ?.
assert (neighborhood V (f x0)).
apply open_neighborhood_is_neighborhood; split; trivial.
pose proof (H0 V H3).
destruct H4 as [U [? ?]].
destruct H4.
pose proof (H U H4 H6).
apply eventually_impl_base with (fun i:DS_set IIn U (x i));
trivial.
intros.
assert (In (inverse_image f V) (x i)); auto with sets.
destruct H9; trivial.
Qed.

Lemma func_preserving_net_limits_is_continuous:
x0:point_set X,
( (I:DirectedSet) (x:Net I X),
net_limit x x0net_limit (fun i:DS_set If (x i)) (f x0))
→ continuous_at f x0.
Proof.
intros.
pose proof (H (neighborhood_net_DS X x0)
(neighborhood_net X x0)
(neighborhood_net_limit X x0)).
apply continuous_at_open_neighborhoods; intros.
destruct H1.
pose proof (H0 V H1 H2).
destruct H3.
destruct x as [U].
U; repeat split; trivial.
pose proof (H3 (intro_neighborhood_net_DS X x0 U x o i H4)).
apply H5.
simpl; auto with sets.
Qed.

End Nets_and_continuity.

Section Subnet.

Variable X:TopologicalSpace.
Variable I:DirectedSet.
Variable x:Net I X.

Inductive Subnet {J:DirectedSet} : Net J XProp :=
| intro_subnet: h:DS_set JDS_set I,
( j1 j2:DS_set J, DS_ord j1 j2
DS_ord (h j1) (h j2)) →
( arbitrarily large i:DS_set I,
j:DS_set J, h j = i) →
Subnet (fun j:DS_set Jx (h j)).

Lemma subnet_limit: (x0:point_set X) {J:DirectedSet}
(y:Net J X), net_limit x x0Subnet y
net_limit y x0.
Proof.
intros.
destruct H0.
red; intros.
pose proof (H U H2 H3).
destruct H4.
destruct (H1 x1).
destruct H5.
destruct H6.
x3.
intros.
apply H4.
apply preord_trans with x2.
apply DS_ord_cond.
assumption.
rewrite <- H6.
apply H0.
assumption.
Qed.

Lemma subnet_cluster_point: (x0:point_set X) {J:DirectedSet}
(y:Net J X), net_cluster_point y x0
Subnet ynet_cluster_point x x0.
Proof.
intros.
destruct H0 as [h h_increasing h_dominant].
red; intros.
red; intros.
pose proof (h_dominant i).
destruct H2.
destruct H2.
destruct H3.
pose proof (H U H0 H1 x2).
destruct H4.
destruct H4.
(h x3).
split; trivial.
apply preord_trans with x1.
apply DS_ord_cond.
assumption.
rewrite <- H3.
apply h_increasing; assumption.
Qed.

Section cluster_point_subnet.

Variable x0:point_set X.
Hypothesis x0_cluster_point: net_cluster_point x x0.
Hypothesis I_nonempty: inhabited (DS_set I).

Record cluster_point_subnet_DS_set : Type := {
cps_i:DS_set I;
cps_U:Ensemble (point_set X);
cps_U_open_neigh: open_neighborhood cps_U x0;
cps_xi_in_U: In cps_U (x cps_i)
}.

Definition cluster_point_subnet_DS_ord
(iU1 iU2 : cluster_point_subnet_DS_set) : Prop :=
DS_ord (cps_i iU1) (cps_i iU2)
Included (cps_U iU2) (cps_U iU1).

Definition cluster_point_subnet_DS : DirectedSet.
refine (Build_DirectedSet
cluster_point_subnet_DS_set
cluster_point_subnet_DS_ord
_ _).
constructor.
red; intros; split; auto with sets.
apply preord_refl.
apply DS_ord_cond.
red; intros.
destruct H; destruct H0.
red; split; auto with sets.
apply preord_trans with (cps_i y); trivial.
apply DS_ord_cond.

intros.
destruct i as [i0 U0 ? ?]; destruct j as [i1 U1 ? ?].
destruct (DS_join_cond i0 i1).
destruct H.
pose proof (x0_cluster_point
(Intersection U0 U1)).
match type of H1 with | __ → ?C
assert C end.
apply H1.
apply open_intersection2;
(apply cps_U_open_neigh0 ||
apply cps_U_open_neigh1).
constructor;
(apply cps_U_open_neigh0 ||
apply cps_U_open_neigh1).
destruct (H2 x1).
destruct H3.
pose (ki := x2).
pose (kU := Intersection U0 U1).
assert (open_neighborhood kU x0).
split.
apply open_intersection2.
apply cps_U_open_neigh0.
apply cps_U_open_neigh1.
constructor; (apply cps_U_open_neigh0 ||
apply cps_U_open_neigh1).
assert (In kU (x ki)).
exact H4.

(Build_cluster_point_subnet_DS_set
ki kU H5 H6).
split; red; simpl; split.
apply preord_trans with x1; trivial.
apply DS_ord_cond.
red; intros.
destruct H7; trivial.
apply preord_trans with x1; trivial.
apply DS_ord_cond.
red; intros.
destruct H7; trivial.
Defined.

Definition cluster_point_subnet : Net
cluster_point_subnet_DS X :=
fun (iU:DS_set cluster_point_subnet_DS) ⇒
x (cps_i iU).

Lemma cluster_point_subnet_is_subnet:
Subnet cluster_point_subnet.
Proof.
constructor.
intros.
destruct j1; destruct j2.
simpl in H; simpl.
red in H; tauto.

red; intros.
i; split.
apply preord_refl; apply DS_ord_cond.
assert (open_neighborhood Full_set x0).
split.
apply open_full.
constructor.
assert (In Full_set (x i)).
constructor.
(Build_cluster_point_subnet_DS_set
i Full_set H H0).
trivial.
Qed.

Lemma cluster_point_subnet_converges:
net_limit cluster_point_subnet x0.
Proof.
red; intros.
destruct I_nonempty as [i0].
destruct (x0_cluster_point U H H0 i0).
destruct H1.
assert (open_neighborhood U x0).
split; trivial.
(Build_cluster_point_subnet_DS_set
x1 U H3 H2).
intros.
destruct j.
red in H4; simpl in H4.
red in H4; simpl in H4.
unfold cluster_point_subnet; simpl.
destruct H4; auto with sets.
Qed.

Lemma net_cluster_point_impl_subnet_converges:
J:DirectedSet, y:Net J X,
Subnet y net_limit y x0.
Proof.
cluster_point_subnet_DS.
cluster_point_subnet.
split.
exact cluster_point_subnet_is_subnet.
exact cluster_point_subnet_converges.
Qed.

End cluster_point_subnet.

End Subnet.