:: On the Baire Category Theorem
:: by Artur Korni{\l}owicz
::
:: Received February 5, 1997
:: Copyright (c) 1997 Association of Mizar Users
Lm1:
for L being non empty RelStr
for f being Function of NAT ,the carrier of L
for n being Element of NAT holds { (f . k) where k is Element of NAT : k <= n } is non empty finite Subset of L
:: deftheorem defines closed WAYBEL12:def 1 :
:: deftheorem Def2 defines dense WAYBEL12:def 2 :
theorem :: WAYBEL12:1
canceled;
theorem Th2: :: WAYBEL12:2
theorem :: WAYBEL12:3
theorem :: WAYBEL12:4
canceled;
theorem :: WAYBEL12:5
canceled;
theorem :: WAYBEL12:6
canceled;
theorem :: WAYBEL12:7
theorem Th8: :: WAYBEL12:8
theorem :: WAYBEL12:9
theorem :: WAYBEL12:10
theorem :: WAYBEL12:11
theorem Th12: :: WAYBEL12:12
theorem Th13: :: WAYBEL12:13
theorem Th14: :: WAYBEL12:14
theorem :: WAYBEL12:15
theorem Th16: :: WAYBEL12:16
theorem :: WAYBEL12:17
theorem Th18: :: WAYBEL12:18
theorem :: WAYBEL12:19
theorem Th20: :: WAYBEL12:20
theorem Th21: :: WAYBEL12:21
theorem :: WAYBEL12:22
theorem Th23: :: WAYBEL12:23
theorem :: WAYBEL12:24
theorem Th25: :: WAYBEL12:25
theorem :: WAYBEL12:26
Lm2:
for L being non empty RelStr
for V being Subset of L holds { x where x is Element of L : V "/\" {x} c= V } is Subset of L
theorem Th27: :: WAYBEL12:27
theorem Th28: :: WAYBEL12:28
theorem Th29: :: WAYBEL12:29
theorem Th30: :: WAYBEL12:30
theorem Th31: :: WAYBEL12:31
theorem :: WAYBEL12:32
Lm3:
for L being Semilattice
for F being Filter of L holds F = uparrow (fininfs F)
:: deftheorem Def3 defines GeneratorSet WAYBEL12:def 3 :
Lm4:
for L being Semilattice
for F being Filter of L
for G being GeneratorSet of F holds G c= F
theorem Th33: :: WAYBEL12:33
theorem Th34: :: WAYBEL12:34
theorem Th35: :: WAYBEL12:35
theorem Th36: :: WAYBEL12:36
theorem Th37: :: WAYBEL12:37
theorem Th38: :: WAYBEL12:38
theorem Th39: :: WAYBEL12:39
theorem Th40: :: WAYBEL12:40
:: deftheorem Def4 defines dense WAYBEL12:def 4 :
theorem :: WAYBEL12:41
:: deftheorem Def5 defines dense WAYBEL12:def 5 :
theorem Th42: :: WAYBEL12:42
theorem Th43: :: WAYBEL12:43
theorem Th44: :: WAYBEL12:44
theorem Th45: :: WAYBEL12:45
theorem Th46: :: WAYBEL12:46
theorem Th47: :: WAYBEL12:47
:: deftheorem defines Baire WAYBEL12:def 6 :
theorem :: WAYBEL12:48