:: On the Boundary and Derivative of a Set
:: by Adam Grabowski
::
:: Received November 8, 2004
:: Copyright (c) 2004 Association of Mizar Users
Lm1:
for T being empty TopSpace
for A being Subset of T holds A = {}
;
theorem Th1: :: TOPGEN_1:1
theorem :: TOPGEN_1:2
canceled;
theorem :: TOPGEN_1:3
theorem :: TOPGEN_1:4
canceled;
theorem Th5: :: TOPGEN_1:5
:: deftheorem Def1 defines Fr TOPGEN_1:def 1 :
theorem :: TOPGEN_1:6
theorem :: TOPGEN_1:7
theorem Th8: :: TOPGEN_1:8
theorem :: TOPGEN_1:9
theorem Th10: :: TOPGEN_1:10
theorem Th11: :: TOPGEN_1:11
theorem :: TOPGEN_1:12
theorem :: TOPGEN_1:13
theorem :: TOPGEN_1:14
theorem :: TOPGEN_1:15
theorem Th16: :: TOPGEN_1:16
:: deftheorem Def2 defines is_an_accumulation_point_of TOPGEN_1:def 2 :
theorem Th17: :: TOPGEN_1:17
:: deftheorem Def3 defines Der TOPGEN_1:def 3 :
theorem Th18: :: TOPGEN_1:18
theorem Th19: :: TOPGEN_1:19
theorem :: TOPGEN_1:20
theorem :: TOPGEN_1:21
:: deftheorem Def4 defines is_isolated_in TOPGEN_1:def 4 :
theorem :: TOPGEN_1:22
theorem Th23: :: TOPGEN_1:23
theorem Th24: :: TOPGEN_1:24
:: deftheorem Def5 defines isolated TOPGEN_1:def 5 :
theorem :: TOPGEN_1:25
:: deftheorem Def6 defines Der TOPGEN_1:def 6 :
theorem :: TOPGEN_1:26
theorem :: TOPGEN_1:27
theorem Th28: :: TOPGEN_1:28
theorem :: TOPGEN_1:29
theorem Th30: :: TOPGEN_1:30
theorem Th31: :: TOPGEN_1:31
theorem Th32: :: TOPGEN_1:32
theorem Th33: :: TOPGEN_1:33
theorem Th34: :: TOPGEN_1:34
theorem Th35: :: TOPGEN_1:35
theorem Th36: :: TOPGEN_1:36
theorem :: TOPGEN_1:37
:: deftheorem Def7 defines dense-in-itself TOPGEN_1:def 7 :
:: deftheorem defines dense-in-itself TOPGEN_1:def 8 :
theorem Th38: :: TOPGEN_1:38
:: deftheorem Def9 defines dense-in-itself TOPGEN_1:def 9 :
theorem Th39: :: TOPGEN_1:39
theorem Th40: :: TOPGEN_1:40
theorem :: TOPGEN_1:41
:: deftheorem Def10 defines perfect TOPGEN_1:def 10 :
theorem Th42: :: TOPGEN_1:42
Lm2:
for T being TopSpace
for A being Subset of T st A is closed & A is dense-in-itself holds
Der A = A
theorem Th43: :: TOPGEN_1:43
theorem Th44: :: TOPGEN_1:44
:: deftheorem Def11 defines scattered TOPGEN_1:def 11 :
theorem Th45: :: TOPGEN_1:45
theorem :: TOPGEN_1:46
theorem Th47: :: TOPGEN_1:47
:: deftheorem Def12 defines density TOPGEN_1:def 12 :
:: deftheorem Def13 defines separable TOPGEN_1:def 13 :
theorem :: TOPGEN_1:48
canceled;
theorem Th49: :: TOPGEN_1:49
theorem :: TOPGEN_1:50
Lm3:
RAT = REAL \ IRRAT
theorem :: TOPGEN_1:51
theorem :: TOPGEN_1:52
theorem :: TOPGEN_1:53
theorem Th54: :: TOPGEN_1:54
theorem Th55: :: TOPGEN_1:55
theorem Th56: :: TOPGEN_1:56
theorem Th57: :: TOPGEN_1:57
theorem Th58: :: TOPGEN_1:58
theorem :: TOPGEN_1:59