:: Basic Properties and Concept of Selected Subsequence of Zero Based FiniteSequences
:: by Yatsuka Nakamura and Hisashi Ito
::
:: Received June 27, 2008
:: Copyright (c) 2008 Association of Mizar Users
theorem Th1: :: AFINSQ_2:1
theorem Th2: :: AFINSQ_2:2
theorem Th3: :: AFINSQ_2:3
theorem Th4: :: AFINSQ_2:4
theorem Th5: :: AFINSQ_2:5
theorem Th6: :: AFINSQ_2:6
theorem Th7: :: AFINSQ_2:7
:: deftheorem Def1 defines Rev AFINSQ_2:def 1 :
theorem Th8: :: AFINSQ_2:8
theorem :: AFINSQ_2:9
theorem Th10: :: AFINSQ_2:10
theorem Th11: :: AFINSQ_2:11
theorem Th12: :: AFINSQ_2:12
theorem Th13: :: AFINSQ_2:13
theorem :: AFINSQ_2:14
:: deftheorem Def2 defines /^ AFINSQ_2:def 2 :
theorem Th15: :: AFINSQ_2:15
theorem Th16: :: AFINSQ_2:16
theorem Th17: :: AFINSQ_2:17
theorem Th18: :: AFINSQ_2:18
theorem Th19: :: AFINSQ_2:19
theorem Th20: :: AFINSQ_2:20
theorem Th21: :: AFINSQ_2:21
theorem :: AFINSQ_2:22
:: deftheorem Def3 defines mid AFINSQ_2:def 3 :
theorem Th23: :: AFINSQ_2:23
theorem :: AFINSQ_2:24
theorem Th25: :: AFINSQ_2:25
theorem :: AFINSQ_2:26
theorem :: AFINSQ_2:27
theorem :: AFINSQ_2:28
:: deftheorem Def4 defines Sum AFINSQ_2:def 4 :
theorem :: AFINSQ_2:29
theorem :: AFINSQ_2:30
definition
let X be
finite natural-membered set ;
func Sgm0 X -> XFinSequence of
means :
Def5:
:: AFINSQ_2:def 5
(
rng it = X & ( for
l,
m,
k1,
k2 being
Nat st
l < m &
m < len it &
k1 = it . l &
k2 = it . m holds
k1 < k2 ) );
existence
ex b1 being XFinSequence of st
( rng b1 = X & ( for l, m, k1, k2 being Nat st l < m & m < len b1 & k1 = b1 . l & k2 = b1 . m holds
k1 < k2 ) )
uniqueness
for b1, b2 being XFinSequence of st rng b1 = X & ( for l, m, k1, k2 being Nat st l < m & m < len b1 & k1 = b1 . l & k2 = b1 . m holds
k1 < k2 ) & rng b2 = X & ( for l, m, k1, k2 being Nat st l < m & m < len b2 & k1 = b2 . l & k2 = b2 . m holds
k1 < k2 ) holds
b1 = b2
end;
:: deftheorem Def5 defines Sgm0 AFINSQ_2:def 5 :
theorem Th31: :: AFINSQ_2:31
theorem Th32: :: AFINSQ_2:32
theorem Th33: :: AFINSQ_2:33
:: deftheorem Def6 defines <N< AFINSQ_2:def 6 :
for
B1,
B2 being
set holds
(
B1 <N< B2 iff for
n,
m being
Nat st
n in B1 &
m in B2 holds
n < m );
:: deftheorem Def7 defines <N= AFINSQ_2:def 7 :
for
B1,
B2 being
set holds
(
B1 <N= B2 iff for
n,
m being
Nat st
n in B1 &
m in B2 holds
n <= m );
theorem Th34: :: AFINSQ_2:34
theorem Th35: :: AFINSQ_2:35
theorem Th36: :: AFINSQ_2:36
theorem :: AFINSQ_2:37
theorem Th38: :: AFINSQ_2:38
theorem :: AFINSQ_2:39
theorem Th40: :: AFINSQ_2:40
theorem Th41: :: AFINSQ_2:41
theorem Th42: :: AFINSQ_2:42
theorem Th43: :: AFINSQ_2:43
theorem Th44: :: AFINSQ_2:44
theorem Th45: :: AFINSQ_2:45
theorem :: AFINSQ_2:46
:: deftheorem defines SubXFinS AFINSQ_2:def 8 :
theorem Th47: :: AFINSQ_2:47
theorem :: AFINSQ_2:48