:: Formal topological spaces
:: by Gang Liu , Yasushi Fuwa and Masayoshi Eguchi
::
:: Received October 13, 2000
:: Copyright (c) 2000 Association of Mizar Users
theorem :: FINTOPO2:1
theorem Th2: :: FINTOPO2:2
theorem :: FINTOPO2:3
theorem :: FINTOPO2:4
theorem :: FINTOPO2:5
:: deftheorem Def1 defines P_1 FINTOPO2:def 1 :
:: deftheorem Def2 defines P_2 FINTOPO2:def 2 :
theorem :: FINTOPO2:6
theorem :: FINTOPO2:7
theorem Th8: :: FINTOPO2:8
:: deftheorem Def3 defines P_0 FINTOPO2:def 3 :
theorem :: FINTOPO2:9
theorem :: FINTOPO2:10
theorem :: FINTOPO2:11
:: deftheorem Def4 defines P_A FINTOPO2:def 4 :
theorem :: FINTOPO2:12
theorem :: FINTOPO2:13
theorem :: FINTOPO2:14
:: deftheorem Def5 defines P_e FINTOPO2:def 5 :
theorem :: FINTOPO2:15
theorem :: FINTOPO2:16
theorem :: FINTOPO2:17
theorem :: FINTOPO2:18
:: deftheorem defines U_FMT FINTOPO2:def 6 :
:: deftheorem defines NeighSp FINTOPO2:def 7 :
:: deftheorem Def8 defines Fo_filled FINTOPO2:def 8 :
:: deftheorem defines ^Fodelta FINTOPO2:def 9 :
theorem :: FINTOPO2:19
canceled;
theorem Th20: :: FINTOPO2:20
:: deftheorem defines ^Fob FINTOPO2:def 10 :
theorem Th21: :: FINTOPO2:21
:: deftheorem defines ^Foi FINTOPO2:def 11 :
theorem Th22: :: FINTOPO2:22
:: deftheorem defines ^Fos FINTOPO2:def 12 :
theorem Th23: :: FINTOPO2:23
:: deftheorem defines ^Fon FINTOPO2:def 13 :
theorem :: FINTOPO2:24
theorem Th25: :: FINTOPO2:25
theorem Th26: :: FINTOPO2:26
theorem Th27: :: FINTOPO2:27
theorem :: FINTOPO2:28
theorem :: FINTOPO2:29
theorem Th30: :: FINTOPO2:30
theorem :: FINTOPO2:31
theorem :: FINTOPO2:32
theorem :: FINTOPO2:33
theorem :: FINTOPO2:34
theorem :: FINTOPO2:35
theorem Th36: :: FINTOPO2:36
theorem Th37: :: FINTOPO2:37
theorem Th38: :: FINTOPO2:38
theorem Th39: :: FINTOPO2:39
theorem Th40: :: FINTOPO2:40
theorem :: FINTOPO2:41
theorem :: FINTOPO2:42
theorem :: FINTOPO2:43
:: deftheorem defines ^Fodel_i FINTOPO2:def 14 :
:: deftheorem defines ^Fodel_o FINTOPO2:def 15 :
theorem :: FINTOPO2:44
:: deftheorem Def16 defines Fo_open FINTOPO2:def 16 :
:: deftheorem Def17 defines Fo_closed FINTOPO2:def 17 :
theorem :: FINTOPO2:45
theorem :: FINTOPO2:46
theorem :: FINTOPO2:47
theorem :: FINTOPO2:48