:: Some Set Series in Finite Topological Spaces. {F}undamental Conceptsfor Image Processing
:: by Masami Tanaka and Yatsuka Nakamura
::
:: Received January 26, 2004
:: Copyright (c) 2004 Association of Mizar Users
:: deftheorem defines ^d FINTOPO3:def 1 :
theorem Th1: :: FINTOPO3:1
theorem Th2: :: FINTOPO3:2
theorem Th3: :: FINTOPO3:3
theorem Th4: :: FINTOPO3:4
theorem Th5: :: FINTOPO3:5
theorem Th6: :: FINTOPO3:6
theorem :: FINTOPO3:7
theorem Th8: :: FINTOPO3:8
theorem :: FINTOPO3:9
theorem Th10: :: FINTOPO3:10
theorem Th11: :: FINTOPO3:11
theorem Th12: :: FINTOPO3:12
:: deftheorem Def2 defines Fcl FINTOPO3:def 2 :
:: deftheorem defines Fcl FINTOPO3:def 3 :
:: deftheorem Def4 defines Fint FINTOPO3:def 4 :
:: deftheorem defines Fint FINTOPO3:def 5 :
theorem :: FINTOPO3:13
theorem :: FINTOPO3:14
theorem Th15: :: FINTOPO3:15
theorem :: FINTOPO3:16
theorem Th17: :: FINTOPO3:17
theorem :: FINTOPO3:18
theorem :: FINTOPO3:19
theorem Th20: :: FINTOPO3:20
theorem :: FINTOPO3:21
theorem Th22: :: FINTOPO3:22
theorem :: FINTOPO3:23
theorem :: FINTOPO3:24
theorem :: FINTOPO3:25
theorem :: FINTOPO3:26
theorem Th27: :: FINTOPO3:27
theorem Th28: :: FINTOPO3:28
theorem :: FINTOPO3:29
theorem :: FINTOPO3:30
:: deftheorem Def6 defines Finf FINTOPO3:def 6 :
:: deftheorem defines Finf FINTOPO3:def 7 :
:: deftheorem Def8 defines Fdfl FINTOPO3:def 8 :
:: deftheorem defines Fdfl FINTOPO3:def 9 :
theorem :: FINTOPO3:31
theorem :: FINTOPO3:32
theorem Th33: :: FINTOPO3:33
theorem :: FINTOPO3:34
theorem :: FINTOPO3:35
theorem :: FINTOPO3:36
theorem :: FINTOPO3:37
theorem :: FINTOPO3:38
theorem :: FINTOPO3:39
theorem Th40: :: FINTOPO3:40
theorem :: FINTOPO3:41
theorem Th42: :: FINTOPO3:42
theorem :: FINTOPO3:43
theorem :: FINTOPO3:44
theorem Th45: :: FINTOPO3:45
theorem :: FINTOPO3:46
:: deftheorem defines U_FT FINTOPO3:def 10 :
theorem :: FINTOPO3:47
theorem :: FINTOPO3:48
:: deftheorem defines are_mutually_symmetric FINTOPO3:def 11 :