:: Some Properties of Cells and Arcsand Adam Naumowicz
:: by Robert Milewski , Andrzej Trybulec , Artur Korni{\l}owicz
::
:: Received October 6, 2000
:: Copyright (c) 2000 Association of Mizar Users
theorem :: JORDAN1B:1
canceled;
theorem :: JORDAN1B:2
theorem :: JORDAN1B:3
theorem Th4: :: JORDAN1B:4
theorem :: JORDAN1B:5
theorem :: JORDAN1B:6
theorem :: JORDAN1B:7
theorem :: JORDAN1B:8
theorem :: JORDAN1B:9
theorem Th10: :: JORDAN1B:10
theorem :: JORDAN1B:11
theorem Th12: :: JORDAN1B:12
theorem :: JORDAN1B:13
theorem Th14: :: JORDAN1B:14
theorem Th15: :: JORDAN1B:15
theorem Th16: :: JORDAN1B:16
theorem :: JORDAN1B:17
theorem Th18: :: JORDAN1B:18
theorem Th19: :: JORDAN1B:19
theorem :: JORDAN1B:20
theorem :: JORDAN1B:21
Lm2:
for i, m being Element of NAT st i <= m & m <= i + 1 & not i = m holds
i = m -' 1
theorem Th22: :: JORDAN1B:22
theorem :: JORDAN1B:23
theorem Th24: :: JORDAN1B:24
theorem :: JORDAN1B:25
theorem :: JORDAN1B:26
canceled;
theorem :: JORDAN1B:27
canceled;
theorem Th28: :: JORDAN1B:28
theorem Th29: :: JORDAN1B:29
theorem :: JORDAN1B:30
theorem :: JORDAN1B:31
theorem Th32: :: JORDAN1B:32
theorem Th33: :: JORDAN1B:33
theorem :: JORDAN1B:34
theorem :: JORDAN1B:35
theorem Th36: :: JORDAN1B:36
theorem Th37: :: JORDAN1B:37
theorem Th38: :: JORDAN1B:38
theorem Th39: :: JORDAN1B:39
Lm3:
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for j, n, i being Element of NAT st j <= width (Gauge C,n) & cell (Gauge C,n),i,j c= BDD C holds
i <> 0
Lm4:
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, n, j being Element of NAT st i <= len (Gauge C,n) & cell (Gauge C,n),i,j c= BDD C holds
j <> 0
Lm5:
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for j, n, i being Element of NAT st j <= width (Gauge C,n) & cell (Gauge C,n),i,j c= BDD C holds
i <> len (Gauge C,n)
Lm6:
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, n, j being Element of NAT st i <= len (Gauge C,n) & cell (Gauge C,n),i,j c= BDD C holds
j <> width (Gauge C,n)
theorem Th40: :: JORDAN1B:40
theorem Th41: :: JORDAN1B:41
theorem Th42: :: JORDAN1B:42
theorem Th43: :: JORDAN1B:43
theorem :: JORDAN1B:44