:: Preliminaries to Mathematical Morphology and Its Properties
:: by Yuzhong Ding and Xiquan Liang
::
:: Received January 7, 2005
:: Copyright (c) 2005 Association of Mizar Users
:: deftheorem defines + MATHMORP:def 1 :
:: deftheorem defines ! MATHMORP:def 2 :
:: deftheorem defines (-) MATHMORP:def 3 :
:: deftheorem defines (+) MATHMORP:def 4 :
theorem Th1: :: MATHMORP:1
theorem Th2: :: MATHMORP:2
theorem Th3: :: MATHMORP:3
theorem Th4: :: MATHMORP:4
theorem :: MATHMORP:5
Lm1:
for n being Element of NAT
for x, y being Point of (TOP-REAL n) holds {x} + y = {y} + x
theorem :: MATHMORP:6
theorem :: MATHMORP:7
theorem Th8: :: MATHMORP:8
theorem Th9: :: MATHMORP:9
theorem Th10: :: MATHMORP:10
theorem :: MATHMORP:11
theorem Th12: :: MATHMORP:12
theorem Th13: :: MATHMORP:13
theorem Th14: :: MATHMORP:14
theorem Th15: :: MATHMORP:15
theorem Th16: :: MATHMORP:16
theorem Th17: :: MATHMORP:17
theorem :: MATHMORP:18
theorem Th19: :: MATHMORP:19
theorem Th20: :: MATHMORP:20
theorem Th21: :: MATHMORP:21
theorem :: MATHMORP:22
Lm2:
for n being Element of NAT
for X, B being Subset of (TOP-REAL n) holds (X (-) B) (+) B c= X
theorem Th23: :: MATHMORP:23
theorem :: MATHMORP:24
theorem :: MATHMORP:25
theorem :: MATHMORP:26
theorem Th27: :: MATHMORP:27
theorem Th28: :: MATHMORP:28
theorem :: MATHMORP:29
theorem :: MATHMORP:30
theorem :: MATHMORP:31
theorem :: MATHMORP:32
theorem :: MATHMORP:33
theorem Th34: :: MATHMORP:34
theorem :: MATHMORP:35
theorem :: MATHMORP:36
theorem Th37: :: MATHMORP:37
theorem Th38: :: MATHMORP:38
:: deftheorem defines (O) MATHMORP:def 5 :
:: deftheorem defines (o) MATHMORP:def 6 :
theorem :: MATHMORP:39
theorem :: MATHMORP:40
theorem Th41: :: MATHMORP:41
theorem Th42: :: MATHMORP:42
theorem :: MATHMORP:43
theorem :: MATHMORP:44
theorem Th45: :: MATHMORP:45
theorem Th46: :: MATHMORP:46
theorem :: MATHMORP:47
theorem :: MATHMORP:48
theorem :: MATHMORP:49
theorem Th50: :: MATHMORP:50
theorem :: MATHMORP:51
theorem :: MATHMORP:52
theorem :: MATHMORP:53
theorem :: MATHMORP:54
theorem :: MATHMORP:55
:: deftheorem defines (.) MATHMORP:def 7 :
theorem :: MATHMORP:56
theorem :: MATHMORP:57
theorem Th58: :: MATHMORP:58
theorem :: MATHMORP:59
theorem Th60: :: MATHMORP:60
theorem Th61: :: MATHMORP:61
theorem Th62: :: MATHMORP:62
theorem Th63: :: MATHMORP:63
theorem Th64: :: MATHMORP:64
theorem :: MATHMORP:65
theorem :: MATHMORP:66
:: deftheorem defines (*) MATHMORP:def 8 :
:: deftheorem defines (&) MATHMORP:def 9 :
:: deftheorem defines (@) MATHMORP:def 10 :
theorem :: MATHMORP:67
theorem :: MATHMORP:68
theorem :: MATHMORP:69
theorem :: MATHMORP:70
theorem :: MATHMORP:71
theorem :: MATHMORP:72
theorem :: MATHMORP:73
canceled;
theorem :: MATHMORP:74
theorem Th75: :: MATHMORP:75
:: deftheorem Def11 defines convex MATHMORP:def 11 :
theorem :: MATHMORP:76
theorem Th77: :: MATHMORP:77
theorem :: MATHMORP:78
theorem :: MATHMORP:79