:: Finite Topological Spaces. Finite Topology Concepts and Neighbourhoods
:: by Hiroshi Imura and Masayoshi Eguchi
::
:: Received November 27, 1992
:: Copyright (c) 1992 Association of Mizar Users
theorem Th1: :: FIN_TOPO:1
theorem Th2: :: FIN_TOPO:2
:: deftheorem defines U_FT FIN_TOPO:def 1 :
:: deftheorem defines SinglRel FIN_TOPO:def 2 :
:: deftheorem defines FT{0} FIN_TOPO:def 3 :
:: deftheorem Def4 defines filled FIN_TOPO:def 4 :
theorem :: FIN_TOPO:3
canceled;
theorem :: FIN_TOPO:4
canceled;
theorem :: FIN_TOPO:5
canceled;
theorem :: FIN_TOPO:6
canceled;
theorem Th7: :: FIN_TOPO:7
theorem :: FIN_TOPO:8
canceled;
theorem :: FIN_TOPO:9
:: deftheorem FIN_TOPO:def 5 :
canceled;
:: deftheorem FIN_TOPO:def 6 :
canceled;
:: deftheorem defines ^delta FIN_TOPO:def 7 :
theorem Th10: :: FIN_TOPO:10
:: deftheorem defines ^deltai FIN_TOPO:def 8 :
:: deftheorem defines ^deltao FIN_TOPO:def 9 :
theorem :: FIN_TOPO:11
:: deftheorem defines ^i FIN_TOPO:def 10 :
:: deftheorem defines ^b FIN_TOPO:def 11 :
:: deftheorem defines ^s FIN_TOPO:def 12 :
:: deftheorem defines ^n FIN_TOPO:def 13 :
:: deftheorem defines ^f FIN_TOPO:def 14 :
:: deftheorem Def15 defines symmetric FIN_TOPO:def 15 :
theorem Th12: :: FIN_TOPO:12
theorem Th13: :: FIN_TOPO:13
theorem Th14: :: FIN_TOPO:14
theorem :: FIN_TOPO:15
theorem Th16: :: FIN_TOPO:16
theorem :: FIN_TOPO:17
:: deftheorem Def16 defines open FIN_TOPO:def 16 :
:: deftheorem Def17 defines closed FIN_TOPO:def 17 :
:: deftheorem Def18 defines connected FIN_TOPO:def 18 :
:: deftheorem defines ^fb FIN_TOPO:def 19 :
:: deftheorem defines ^fi FIN_TOPO:def 20 :
theorem Th18: :: FIN_TOPO:18
theorem Th19: :: FIN_TOPO:19
theorem :: FIN_TOPO:20
theorem :: FIN_TOPO:21
canceled;
theorem Th22: :: FIN_TOPO:22
theorem Th23: :: FIN_TOPO:23
theorem :: FIN_TOPO:24
theorem :: FIN_TOPO:25
theorem :: FIN_TOPO:26
theorem :: FIN_TOPO:27
theorem :: FIN_TOPO:28
theorem :: FIN_TOPO:29
canceled;
theorem :: FIN_TOPO:30
theorem :: FIN_TOPO:31