coq-topology/SubspaceTopology.v at master · dschepler/coq-topology · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
Require Export TopologicalSpaces.
Require Import WeakTopology.

Section Subspace.

Variable X:TopologicalSpace.
Variable A:Ensemble (point_set X).

Definition SubspaceTopology : TopologicalSpace :=
  WeakTopology1 (proj1_sig (P:=fun x:point_set X => In A x)).

Definition subspace_inc : point_set SubspaceTopology ->
  point_set X :=
  proj1_sig (P:=fun x:point_set X => In A x).

Lemma subspace_topology_topology: forall U:Ensemble {x:point_set X | In A x},
  @open SubspaceTopology U -> exists V:Ensemble (point_set X),
  open V /\ U = inverse_image subspace_inc V.
Proof.
apply weak_topology1_topology.
Qed.

Lemma subspace_inc_continuous:
  continuous subspace_inc.
Proof.
apply weak_topology1_makes_continuous_func.
Qed.

End Subspace.

Implicit Arguments SubspaceTopology [[X]].
Implicit Arguments subspace_inc [[X]].