:: Continuity of Mappings over the Union of Subspaces
:: by Zbigniew Karno
::
:: Received May 22, 1992
:: Copyright (c) 1992 Association of Mizar Users
:: deftheorem Def1 defines union TMAP_1:def 1 :
theorem :: TMAP_1:1
canceled;
theorem :: TMAP_1:2
canceled;
theorem :: TMAP_1:3
canceled;
theorem :: TMAP_1:4
canceled;
theorem :: TMAP_1:5
canceled;
theorem Th6: :: TMAP_1:6
theorem Th7: :: TMAP_1:7
theorem :: TMAP_1:8
theorem :: TMAP_1:9
for
A,
B being non
empty set for
A1,
A2,
A3,
A12,
A23 being non
empty Subset of
A st
A12 = A1 \/ A2 &
A23 = A2 \/ A3 holds
for
f1 being
Function of
A1,
B for
f2 being
Function of
A2,
B for
f3 being
Function of
A3,
B st
f1 | (A1 /\ A2) = f2 | (A1 /\ A2) &
f2 | (A2 /\ A3) = f3 | (A2 /\ A3) &
f1 | (A1 /\ A3) = f3 | (A1 /\ A3) holds
for
f12 being
Function of
A12,
B for
f23 being
Function of
A23,
B st
f12 = f1 union f2 &
f23 = f2 union f3 holds
f12 union f3 = f1 union f23
theorem :: TMAP_1:10
Lm1:
for X being TopSpace holds TopStruct(# the carrier of X,the topology of X #) is TopSpace-like
theorem Th11: :: TMAP_1:11
theorem Th12: :: TMAP_1:12
theorem Th13: :: TMAP_1:13
theorem Th14: :: TMAP_1:14
theorem Th15: :: TMAP_1:15
theorem Th16: :: TMAP_1:16
theorem Th17: :: TMAP_1:17
theorem :: TMAP_1:18
theorem Th19: :: TMAP_1:19
theorem Th20: :: TMAP_1:20
theorem Th21: :: TMAP_1:21
theorem Th22: :: TMAP_1:22
theorem Th23: :: TMAP_1:23
theorem Th24: :: TMAP_1:24
theorem :: TMAP_1:25
theorem :: TMAP_1:26
theorem Th27: :: TMAP_1:27
theorem :: TMAP_1:28
theorem Th29: :: TMAP_1:29
theorem :: TMAP_1:30
theorem Th31: :: TMAP_1:31
theorem Th32: :: TMAP_1:32
theorem Th33: :: TMAP_1:33
theorem Th34: :: TMAP_1:34
theorem Th35: :: TMAP_1:35
theorem Th36: :: TMAP_1:36
theorem Th37: :: TMAP_1:37
theorem Th38: :: TMAP_1:38
theorem Th39: :: TMAP_1:39
theorem :: TMAP_1:40
theorem :: TMAP_1:41
theorem :: TMAP_1:42
theorem Th43: :: TMAP_1:43
theorem Th44: :: TMAP_1:44
theorem :: TMAP_1:45
theorem Th46: :: TMAP_1:46
:: deftheorem Def2 defines is_continuous_at TMAP_1:def 2 :
theorem Th47: :: TMAP_1:47
theorem Th48: :: TMAP_1:48
theorem Th49: :: TMAP_1:49
theorem Th50: :: TMAP_1:50
theorem Th51: :: TMAP_1:51
theorem Th52: :: TMAP_1:52
theorem :: TMAP_1:53
theorem :: TMAP_1:54
theorem :: TMAP_1:55
theorem Th56: :: TMAP_1:56
theorem :: TMAP_1:57
:: deftheorem defines | TMAP_1:def 3 :
theorem :: TMAP_1:58
canceled;
theorem Th59: :: TMAP_1:59
theorem Th60: :: TMAP_1:60
theorem :: TMAP_1:61
theorem :: TMAP_1:62
theorem Th63: :: TMAP_1:63
theorem Th64: :: TMAP_1:64
theorem Th65: :: TMAP_1:65
theorem Th66: :: TMAP_1:66
theorem :: TMAP_1:67
theorem Th68: :: TMAP_1:68
theorem Th69: :: TMAP_1:69
theorem Th70: :: TMAP_1:70
theorem :: TMAP_1:71
:: deftheorem Def4 defines | TMAP_1:def 4 :
theorem Th72: :: TMAP_1:72
theorem :: TMAP_1:73
theorem Th74: :: TMAP_1:74
theorem Th75: :: TMAP_1:75
theorem :: TMAP_1:76
theorem Th77: :: TMAP_1:77
theorem Th78: :: TMAP_1:78
theorem Th79: :: TMAP_1:79
theorem :: TMAP_1:80
theorem Th81: :: TMAP_1:81
theorem Th82: :: TMAP_1:82
theorem Th83: :: TMAP_1:83
theorem Th84: :: TMAP_1:84
theorem :: TMAP_1:85
theorem Th86: :: TMAP_1:86
theorem :: TMAP_1:87
theorem Th88: :: TMAP_1:88
theorem Th89: :: TMAP_1:89
theorem Th90: :: TMAP_1:90
theorem :: TMAP_1:91
theorem :: TMAP_1:92
theorem :: TMAP_1:93
theorem Th94: :: TMAP_1:94
:: deftheorem TMAP_1:def 5 :
canceled;
:: deftheorem defines incl TMAP_1:def 6 :
theorem :: TMAP_1:95
theorem :: TMAP_1:96
theorem :: TMAP_1:97
theorem :: TMAP_1:98
:: deftheorem defines -extension_of_the_topology_of TMAP_1:def 7 :
theorem Th99: :: TMAP_1:99
theorem Th100: :: TMAP_1:100
theorem Th101: :: TMAP_1:101
theorem Th102: :: TMAP_1:102
theorem Th103: :: TMAP_1:103
:: deftheorem defines modified_with_respect_to TMAP_1:def 8 :
theorem :: TMAP_1:104
theorem Th105: :: TMAP_1:105
theorem Th106: :: TMAP_1:106
:: deftheorem defines modid TMAP_1:def 9 :
theorem :: TMAP_1:107
canceled;
theorem Th108: :: TMAP_1:108
theorem Th109: :: TMAP_1:109
theorem Th110: :: TMAP_1:110
theorem Th111: :: TMAP_1:111
theorem Th112: :: TMAP_1:112
theorem Th113: :: TMAP_1:113
:: deftheorem Def10 defines modified_with_respect_to TMAP_1:def 10 :
theorem Th114: :: TMAP_1:114
theorem :: TMAP_1:115
theorem :: TMAP_1:116
:: deftheorem Def11 defines modid TMAP_1:def 11 :
theorem :: TMAP_1:117
theorem Th118: :: TMAP_1:118
theorem Th119: :: TMAP_1:119
theorem :: TMAP_1:120
theorem :: TMAP_1:121
theorem :: TMAP_1:122
theorem Th123: :: TMAP_1:123
theorem :: TMAP_1:124
theorem :: TMAP_1:125
theorem Th126: :: TMAP_1:126
theorem Th127: :: TMAP_1:127
theorem Th128: :: TMAP_1:128
theorem Th129: :: TMAP_1:129
theorem :: TMAP_1:130
theorem :: TMAP_1:131
theorem Th132: :: TMAP_1:132
theorem Th133: :: TMAP_1:133
theorem Th134: :: TMAP_1:134
theorem Th135: :: TMAP_1:135
theorem Th136: :: TMAP_1:136
theorem :: TMAP_1:137
:: deftheorem Def12 defines union TMAP_1:def 12 :
theorem Th138: :: TMAP_1:138
theorem :: TMAP_1:139
theorem Th140: :: TMAP_1:140
theorem :: TMAP_1:141
theorem :: TMAP_1:142
theorem :: TMAP_1:143
theorem :: TMAP_1:144
theorem Th145: :: TMAP_1:145
theorem :: TMAP_1:146
theorem :: TMAP_1:147
theorem :: TMAP_1:148
theorem :: TMAP_1:149
theorem :: TMAP_1:150
theorem :: TMAP_1:151
theorem :: TMAP_1:152
theorem :: TMAP_1:153