:: Finite Sets
:: by Agata Darmochwa\l
::
:: Received April 6, 1989
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem Def1 defines finite FINSET_1:def 1 :
Lm1:
for x being set holds {x} is finite
Lm2:
for A, B being set st A is finite & B is finite holds
A \/ B is finite
registration
let x1,
x2,
x3,
x4,
x5 be
set ;
cluster {x1,x2,x3,x4,x5} -> finite ;
coherence
{x1,x2,x3,x4,x5} is finite
end;
registration
let x1,
x2,
x3,
x4,
x5,
x6 be
set ;
cluster {x1,x2,x3,x4,x5,x6} -> finite ;
coherence
{x1,x2,x3,x4,x5,x6} is finite
end;
registration
let x1,
x2,
x3,
x4,
x5,
x6,
x7 be
set ;
cluster {x1,x2,x3,x4,x5,x6,x7} -> finite ;
coherence
{x1,x2,x3,x4,x5,x6,x7} is finite
end;
registration
let x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 be
set ;
cluster {x1,x2,x3,x4,x5,x6,x7,x8} -> finite ;
coherence
{x1,x2,x3,x4,x5,x6,x7,x8} is finite
end;
theorem :: FINSET_1:1
canceled;
theorem :: FINSET_1:2
canceled;
theorem :: FINSET_1:3
canceled;
theorem :: FINSET_1:4
canceled;
theorem :: FINSET_1:5
canceled;
theorem :: FINSET_1:6
canceled;
theorem :: FINSET_1:7
canceled;
theorem :: FINSET_1:8
canceled;
theorem :: FINSET_1:9
canceled;
theorem :: FINSET_1:10
canceled;
theorem :: FINSET_1:11
canceled;
theorem :: FINSET_1:12
canceled;
theorem Th13: :: FINSET_1:13
theorem :: FINSET_1:14
theorem :: FINSET_1:15
theorem :: FINSET_1:16
theorem Th17: :: FINSET_1:17
theorem Th18: :: FINSET_1:18
Lm3:
for A being set st A is finite & ( for X being set st X in A holds
X is finite ) holds
union A is finite
theorem :: FINSET_1:19
canceled;
theorem :: FINSET_1:20
canceled;
theorem :: FINSET_1:21
canceled;
theorem :: FINSET_1:22
canceled;
theorem :: FINSET_1:23
canceled;
theorem :: FINSET_1:24
canceled;
theorem :: FINSET_1:25
theorem Th26: :: FINSET_1:26
theorem :: FINSET_1:27
theorem :: FINSET_1:28
canceled;
theorem Th29: :: FINSET_1:29
theorem :: FINSET_1:30
theorem :: FINSET_1:31
:: deftheorem defines finite-yielding FINSET_1:def 2 :
deffunc H1( set ) -> set = $1 `1 ;
theorem :: FINSET_1:32
theorem :: FINSET_1:33
:: deftheorem defines centered FINSET_1:def 3 :