Definition: ss-homeo
`ss-homeo(X;Y) ==  ∃f:Point(X ⟶ Y). ∃g:Point(Y ⟶ X). ((∀x:Point(X). g(f(x)) ≡ x) ∧ (∀y:Point(Y). f(g(y)) ≡ y))`

Lemma: ss-homeo_wf
`∀[X,Y:SeparationSpace].  (ss-homeo(X;Y) ∈ ℙ)`

Lemma: ss-homeo_weakening
`∀[X,Y:SeparationSpace].  ss-homeo(X;Y) supposing X = Y ∈ SeparationSpace`

Lemma: ss-homeo_inversion
`∀[X,Y:SeparationSpace].  (ss-homeo(X;Y) `` ss-homeo(Y;X))`

Lemma: ss-homeo_transitivity
`∀[X,Y,Z:SeparationSpace].  (ss-homeo(X;Y) `` ss-homeo(Y;Z) `` ss-homeo(X;Z))`

Lemma: ss-fun-fun
`∀[X,Y,Z:SeparationSpace].  ss-homeo(X ⟶ Y ⟶ Z;X × Y ⟶ Z)`

Lemma: ss-prod-prod
`∀[X,Y,Z:SeparationSpace].  ss-homeo(X × Y × Z;X × Y × Z)`

Lemma: unit-ss-eq
`∀[t,t':{t:ℝ| t ∈ [r0, r1]} ].  uiff(t = t';t ≡ t')`

Definition: path-ss
`Path(X) ==  𝕀 ⟶ X`

Lemma: path-ss_wf
`∀[X:SeparationSpace]. (Path(X) ∈ SeparationSpace)`

Lemma: path-ss-point
`∀[X:Top]`
`  (Point(Path(X)) ~ {f:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)}  ⟶ Point(X)| ∀t,t':{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} .  (t ≡ t' `` f t ≡ f t\000C')} )`

Definition: path-at
`p@t ==  p t`

Lemma: path-at_wf
`∀[X:SeparationSpace]. ∀[p:Point(Path(X))]. ∀[t:{t:ℝ| t ∈ [r0, r1]} ].  (p@t ∈ Point(X))`

Lemma: path-at_functionality
`∀[X:SeparationSpace]. ∀[p:Point(Path(X))]. ∀[t,t':{t:ℝ| t ∈ [r0, r1]} ].  p@t ≡ p@t' supposing t = t'`

Lemma: path-at_functionality2
`∀[X:SeparationSpace]. ∀[p:Point(Path(X))]. ∀[t,t':{t:ℝ| t ∈ [r0, r1]} ].  p@t ≡ p@t' supposing t ≡ t'`

Definition: ss-free-homotopic
`ss-free-homotopic(X;a;b) ==  ∃p:Point(Path(X)). (p@r0 ≡ a ∧ p@r1 ≡ b)`

Lemma: ss-free-homotopic_wf
`∀[X:SeparationSpace]. ∀[a,b:Point(X)].  (ss-free-homotopic(X;a;b) ∈ ℙ)`

Lemma: ss-free-homotopic_weakening
`∀X:SeparationSpace. ∀a,b:Point(X).  ss-free-homotopic(X;a;b) supposing a ≡ b`

Lemma: ss-free-homotopic_inversion
`∀X:SeparationSpace. ∀a,b:Point(X).  (ss-free-homotopic(X;a;b) `` ss-free-homotopic(X;b;a))`

Definition: ss-homotopic
`ss-homotopic(X;x0;x1;a;b) ==`
`  ∃p:Point(Path(Path(X))). (p@r0 ≡ a ∧ p@r1 ≡ b ∧ (∀t:{t:ℝ| t ∈ [r0, r1]} . (p@t@r0 ≡ x0 ∧ p@t@r1 ≡ x1)))`

Lemma: ss-homotopic_wf
`∀[X:SeparationSpace]. ∀[x0,x1:Point(X)]. ∀[a,b:Point(Path(X))].  (ss-homotopic(X;x0;x1;a;b) ∈ ℙ)`

Lemma: ss-homotopic_weakening
`∀X:SeparationSpace`
`  ∀[x0,x1:Point(X)].  ∀a,b:Point(Path(X)).  (ss-homotopic(X;x0;x1;a;b)) supposing (a ≡ b and b@r0 ≡ x0 and b@r1 ≡ x1)`

Lemma: ss-homotopic_inversion
`∀X:SeparationSpace. ∀[x0,x1:Point(X)].  ∀a,b:Point(Path(X)).  (ss-homotopic(X;x0;x1;a;b) `` ss-homotopic(X;x0;x1;b;a))`

Definition: path-comp-rel
`path-comp-rel(X;f;g;h) ==`
`  (∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . h@t ≡ f@r(2) * t) ∧ (∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . h@t ≡ g@(r(2) * t) - r1)`

Lemma: path-comp-rel_wf
`∀[X:SeparationSpace]. ∀[f,g,h:Point(Path(X))].  (path-comp-rel(X;f;g;h) ∈ ℙ)`

Definition: path-comp-property
`path-comp-property(X) ==  ∀f,g:Point(Path(X)).  (f@r1 ≡ g@r0 `` (∃h:Point(Path(X)). path-comp-rel(X;f;g;h)))`

Lemma: path-comp-property_wf
`∀[X:SeparationSpace]. (path-comp-property(X) ∈ ℙ)`

Lemma: path-comp-property_functionality
`∀[X,Y:SeparationSpace].  (ss-homeo(X;Y) `` (path-comp-property(X) `⇐⇒` path-comp-property(Y)))`

Lemma: path-comp-for-reals
`path-comp-property(ℝ)`

Lemma: path-comp-prod
`∀[A,B:SeparationSpace].  (path-comp-property(A) `` path-comp-property(B) `` path-comp-property(A × B))`

Lemma: path-in-union
`∀[A,B:SeparationSpace].`
`  ∀f:Point(Path(A + B))`
`    (((∀x:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} . (↑isl(f@x))) ∧ (λx.outl(f x) ∈ Point(Path(A))))`
`    ∨ ((∀x:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} . (↑isr(f@x))) ∧ (λx.outr(f x) ∈ Point(Path(B)))))`

Lemma: path-comp-union
`∀[A,B:SeparationSpace].  (path-comp-property(A) `` path-comp-property(B) `` path-comp-property(A + B))`

Lemma: path-comp-fun
`∀[T:Type]. ∀[B:SeparationSpace].  (path-comp-property(B) `` path-comp-property(T ⟶ B))`

Lemma: path-comp-set
`∀[A:SeparationSpace]. ∀[P:Point(A) ⟶ ℙ].`
`  ((∀a:Point(A). Stable{P[a]})`
`  `` (∀a,b:Point(A).  (a ≡ b `` P[b] `` P[a]))`
`  `` path-comp-property(A)`
`  `` path-comp-property({a:A | P[a]}))`

Definition: ss-basic
`ss-basic(X) ==  (Point(X ⟶ ℝ) × ℝ) List`

Lemma: ss-basic_wf
`∀[X:SeparationSpace]. (ss-basic(X) ∈ Type)`

Definition: ss-mem-basic
`x ∈ B ==  (∀p∈B.let f,r = p in f(x) < r)`

Lemma: ss-mem-basic_wf
`∀[X:SeparationSpace]. ∀[B:ss-basic(X)]. ∀[x:Point(X)].  (x ∈ B ∈ ℙ)`

Lemma: sq_stable__ss-mem-basic
`∀[X:SeparationSpace]. ∀B:ss-basic(X). ∀x:Point(X).  SqStable(x ∈ B)`

Definition: ss-open
`Open(X) ==  ss-basic(X) ⟶ ℙ`

Lemma: ss-open_wf
`∀[X:SeparationSpace]. (Open(X) ∈ 𝕌')`

Definition: ss-mem-open
`x ∈ O ==  ∃B:ss-basic(X). ((O B) ∧ x ∈ B)`

Lemma: ss-mem-open_wf
`∀[X:SeparationSpace]. ∀[O:Open(X)]. ∀[x:Point(X)].  (x ∈ O ∈ ℙ)`

Definition: ss-empty
`ss-empty() ==  λB.False`

Lemma: ss-empty_wf
`∀[X:SeparationSpace]. (ss-empty() ∈ Open(X))`

Lemma: ss-mem-empty
`∀[X:SeparationSpace]. ∀[x:Point(X)].  uiff(x ∈ ss-empty();False)`

Definition: ss-basic-whole
`ss-basic-whole() ==  [<ss-const(r0), r1>]`

Lemma: ss-basic-whole_wf
`∀[X:SeparationSpace]. (ss-basic-whole() ∈ ss-basic(X))`

Definition: ss-basic-and
`ss-basic-and(u;v) ==  u @ v`

Lemma: ss-basic-and_wf
`∀[X:SeparationSpace]. ∀[u,v:ss-basic(X)].  (ss-basic-and(u;v) ∈ ss-basic(X))`

Lemma: ss-mem-basic-and
`∀[X:SeparationSpace]. ∀u,v:ss-basic(X). ∀x:Point(X).  uiff(x ∈ ss-basic-and(u;v);x ∈ u ∧ x ∈ v)`

Lemma: ss-mem-basic-whole
`∀X:SeparationSpace. ∀x:Point(X).  uiff(x ∈ ss-basic-whole();True)`

Definition: ss-whole
`ss-whole(X) ==  λB.(B = ss-basic-whole() ∈ ss-basic(X))`

Lemma: ss-whole_wf
`∀[X:SeparationSpace]. (ss-whole(X) ∈ Open(X))`

Lemma: ss-mem-whole
`∀X:SeparationSpace. ∀x:Point(X).  uiff(x ∈ ss-whole(X);True)`

Definition: ss-open-and
`A ⋂ B ==  λz.∃u,v:ss-basic(X). ((A u) ∧ (B v) ∧ (z = ss-basic-and(u;v) ∈ ss-basic(X)))`

Lemma: ss-open-and_wf
`∀[X:SeparationSpace]. ∀[A,B:Open(X)].  (A ⋂ B ∈ Open(X))`

Lemma: ss-mem-open-and
`∀[X:SeparationSpace]. ∀A,B:Open(X). ∀x:Point(X).  (x ∈ A ⋂ B `⇐⇒` x ∈ A ∧ x ∈ B)`

Definition: ss-open-or
`⋃x:T.F[x] ==  λB.∃x:T. (F[x] B)`

Lemma: ss-open-or_wf
`∀[X:SeparationSpace]. ∀[T:Type]. ∀[F:T ⟶ Open(X)].  (⋃x:T.F[x] ∈ Open(X))`

Lemma: ss-mem-open-or
`∀[X:SeparationSpace]. ∀T:Type. ∀F:T ⟶ Open(X). ∀x:Point(X).  (x ∈ ⋃t:T.F[t] `⇐⇒` ∃t:T. x ∈ F[t])`

Lemma: path-end-mem-basic
`∀X:SeparationSpace. ∀f:Point(Path(X)). ∀B:ss-basic(X).`
`  (f@r1 ∈ B `` (∃z:{z:ℝ| z ∈ [r0, r1)} . ∀t:{t:ℝ| t ∈ [z, r1]} . f@t ∈ B))`

Lemma: path-end-mem-open
`∀X:SeparationSpace. ∀f:Point(Path(X)). ∀O:Open(X).`
`  (f@r1 ∈ O `` (∃z:{z:ℝ| z ∈ [r0, r1)} . ∀t:{t:ℝ| t ∈ [z, r1]} . f@t ∈ O))`

Home Index