:: BORSUK_3 semantic presentation
theorem Th1: :: BORSUK_3:1
theorem Th2: :: BORSUK_3:2
Lemma3:
for b1 being non empty TopStruct holds b1,b1 are_homeomorphic
Lemma4:
for b1, b2 being non empty TopStruct st b1,b2 are_homeomorphic holds
b2,b1 are_homeomorphic
theorem Th3: :: BORSUK_3:3
theorem Th4: :: BORSUK_3:4
theorem Th5: :: BORSUK_3:5
theorem Th6: :: BORSUK_3:6
theorem Th7: :: BORSUK_3:7
theorem Th8: :: BORSUK_3:8
theorem Th9: :: BORSUK_3:9
theorem Th10: :: BORSUK_3:10
theorem Th11: :: BORSUK_3:11
theorem Th12: :: BORSUK_3:12
theorem Th13: :: BORSUK_3:13
theorem Th14: :: BORSUK_3:14
theorem Th15: :: BORSUK_3:15
Lemma15:
for b1, b2 being non empty TopSpace
for b3 being Point of b1
for b4 being non empty Subset of b1 st b4 = {b3} holds
[:b2,(b1 | b4):],b2 are_homeomorphic
theorem Th16: :: BORSUK_3:16
theorem Th17: :: BORSUK_3:17
Lemma18:
for b1, b2 being TopSpace
for b3 being Subset of [:b2,b1:]
for b4 being Subset of b1 st b3 = [:([#] b2),b4:] holds
TopStruct(# the carrier of [:b2,(b1 | b4):],the topology of [:b2,(b1 | b4):] #) = TopStruct(# the carrier of ([:b2,b1:] | b3),the topology of ([:b2,b1:] | b3) #)
theorem Th18: :: BORSUK_3:18
theorem Th19: :: BORSUK_3:19
theorem Th20: :: BORSUK_3:20
theorem Th21: :: BORSUK_3:21
theorem Th22: :: BORSUK_3:22
theorem Th23: :: BORSUK_3:23
Lemma23:
for b1, b2 being non empty compact TopSpace holds [:b1,b2:] is compact
theorem Th24: :: BORSUK_3:24
Lemma25:
for b1, b2 being TopSpace
for b3 being SubSpace of b1 holds [:b3,b2:] is SubSpace of [:b1,b2:]
theorem Th25: :: BORSUK_3:25
theorem Th26: :: BORSUK_3:26
theorem Th27: :: BORSUK_3:27