:: Baire Spaces, Sober Spaces
:: by Andrzej Trybulec
::
:: Received January 8, 1997
:: Copyright (c) 1997 Association of Mizar Users
theorem Th1: :: YELLOW_8:1
theorem Th2: :: YELLOW_8:2
:: deftheorem Def1 defines trivial YELLOW_8:def 1 :
theorem :: YELLOW_8:3
canceled;
theorem Th4: :: YELLOW_8:4
theorem Th5: :: YELLOW_8:5
theorem :: YELLOW_8:6
canceled;
theorem :: YELLOW_8:7
canceled;
theorem :: YELLOW_8:8
canceled;
theorem :: YELLOW_8:9
canceled;
theorem :: YELLOW_8:10
canceled;
theorem :: YELLOW_8:11
canceled;
theorem :: YELLOW_8:12
canceled;
theorem :: YELLOW_8:13
canceled;
theorem :: YELLOW_8:14
theorem Th15: :: YELLOW_8:15
theorem Th16: :: YELLOW_8:16
theorem :: YELLOW_8:17
theorem Th18: :: YELLOW_8:18
theorem Th19: :: YELLOW_8:19
theorem :: YELLOW_8:20
:: deftheorem Def2 defines Basis YELLOW_8:def 2 :
theorem Th21: :: YELLOW_8:21
theorem :: YELLOW_8:22
theorem :: YELLOW_8:23
:: deftheorem Def3 defines Baire YELLOW_8:def 3 :
theorem :: YELLOW_8:24
:: deftheorem Def4 defines irreducible YELLOW_8:def 4 :
:: deftheorem Def5 defines is_dense_point_of YELLOW_8:def 5 :
theorem :: YELLOW_8:25
theorem Th26: :: YELLOW_8:26
:: deftheorem Def6 defines sober YELLOW_8:def 6 :
theorem Th27: :: YELLOW_8:27
theorem Th28: :: YELLOW_8:28
theorem Th29: :: YELLOW_8:29
theorem Th30: :: YELLOW_8:30
theorem Th31: :: YELLOW_8:31
theorem Th32: :: YELLOW_8:32
theorem Th33: :: YELLOW_8:33
:: deftheorem Def7 defines CofinTop YELLOW_8:def 7 :
theorem Th34: :: YELLOW_8:34
theorem Th35: :: YELLOW_8:35
theorem Th36: :: YELLOW_8:36
theorem :: YELLOW_8:37