:: Preliminaries to Polynomials
:: by Andrzej Trybulec
::
:: Received August 7, 2009
:: Copyright (c) 2009 Association of Mizar Users
:: deftheorem Def14 defines FlattenSeq PRE_POLY:def 1 :
theorem Th13D: :: PRE_POLY:1
theorem Th20D: :: PRE_POLY:2
theorem Th21D: :: PRE_POLY:3
theorem :: PRE_POLY:4
theorem :: PRE_POLY:5
theorem :: PRE_POLY:6
theorem :: PRE_POLY:7
theorem Th3: :: PRE_POLY:8
definition
let X be
set ;
let A be
finite Subset of
X;
let R be
Order of
X;
assume A1:
R linearly_orders A
;
func SgmX R,
A -> FinSequence of
X means :
Def2T:
:: PRE_POLY:def 2
(
rng it = A & ( for
n,
m being
Nat st
n in dom it &
m in dom it &
n < m holds
(
it /. n <> it /. m &
[(it /. n),(it /. m)] in R ) ) );
existence
ex b1 being FinSequence of X st
( rng b1 = A & ( for n, m being Nat st n in dom b1 & m in dom b1 & n < m holds
( b1 /. n <> b1 /. m & [(b1 /. n),(b1 /. m)] in R ) ) )
uniqueness
for b1, b2 being FinSequence of X st rng b1 = A & ( for n, m being Nat st n in dom b1 & m in dom b1 & n < m holds
( b1 /. n <> b1 /. m & [(b1 /. n),(b1 /. m)] in R ) ) & rng b2 = A & ( for n, m being Nat st n in dom b2 & m in dom b2 & n < m holds
( b2 /. n <> b2 /. m & [(b2 /. n),(b2 /. m)] in R ) ) holds
b1 = b2
end;
:: deftheorem Def2T defines SgmX PRE_POLY:def 2 :
theorem :: PRE_POLY:9
theorem Th8T: :: PRE_POLY:10
theorem :: PRE_POLY:11
theorem Th3: :: PRE_POLY:12
theorem :: PRE_POLY:13
:: deftheorem Def1M defines FinSequence-yielding PRE_POLY:def 3 :
:: deftheorem Def2M defines ^^ PRE_POLY:def 4 :
theorem :: PRE_POLY:14
theorem :: PRE_POLY:15
theorem Th4: :: PRE_POLY:16
theorem Th5: :: PRE_POLY:17
theorem Th4: :: PRE_POLY:18
theorem Th7: :: PRE_POLY:19
theorem Th8: :: PRE_POLY:20
theorem Th9: :: PRE_POLY:21
theorem Th10: :: PRE_POLY:22
theorem Th11: :: PRE_POLY:23
theorem Th12: :: PRE_POLY:24
theorem Th13: :: PRE_POLY:25
theorem Th14: :: PRE_POLY:26
theorem Th30: :: PRE_POLY:27
theorem Th31: :: PRE_POLY:28
theorem Th32: :: PRE_POLY:29
theorem Th33: :: PRE_POLY:30
theorem Th35: :: PRE_POLY:31
theorem :: PRE_POLY:32
:: deftheorem Def5 defines + PRE_POLY:def 5 :
:: deftheorem Def6 defines -' PRE_POLY:def 6 :
theorem :: PRE_POLY:33
theorem Th38: :: PRE_POLY:34
theorem Th39: :: PRE_POLY:35
theorem :: PRE_POLY:36
:: deftheorem Def7 defines support PRE_POLY:def 7 :
theorem Th41: :: PRE_POLY:37
:: deftheorem Def8 defines finite-support PRE_POLY:def 8 :
theorem Th42: :: PRE_POLY:38
theorem Th43: :: PRE_POLY:39
theorem Th44: :: PRE_POLY:40
:: deftheorem Def11 defines < PRE_POLY:def 9 :
theorem Th45: :: PRE_POLY:41
for
n being
Ordinal for
p,
q,
r being
bag of st
p < q &
q < r holds
p < r
:: deftheorem Def12 defines <=' PRE_POLY:def 10 :
for
n being
Ordinal for
p,
q being
bag of holds
(
p <=' q iff (
p < q or
p = q ) );
theorem Th46: :: PRE_POLY:42
theorem :: PRE_POLY:43
for
n being
Ordinal for
p,
q,
r being
bag of st
p < q &
q <=' r holds
p < r
theorem :: PRE_POLY:44
for
n being
Ordinal for
p,
q,
r being
bag of st
p <=' q &
q < r holds
p < r
theorem Th49: :: PRE_POLY:45
:: deftheorem Def13 defines divides PRE_POLY:def 11 :
for
X being
set for
d,
b being
bag of holds
(
d divides b iff for
k being
set holds
d . k <= b . k );
theorem Th50: :: PRE_POLY:46
theorem Th51: :: PRE_POLY:47
theorem Th52: :: PRE_POLY:48
for
X being
set for
b1,
b2 being
bag of holds
(b2 + b1) -' b1 = b2
theorem Th53: :: PRE_POLY:49
theorem Th54: :: PRE_POLY:50
for
n being
set for
b,
b1,
b2 being
bag of st
b = b1 + b2 holds
b1 divides b
:: deftheorem Def14 defines Bags PRE_POLY:def 12 :
for
X being
set for
b2 being
set holds
(
b2 = Bags X iff for
x being
set holds
(
x in b2 iff
x is
bag of ) );
theorem :: PRE_POLY:51
:: deftheorem defines EmptyBag PRE_POLY:def 13 :
theorem Th56: :: PRE_POLY:52
theorem :: PRE_POLY:53
theorem Th58: :: PRE_POLY:54
theorem :: PRE_POLY:55
theorem Th60: :: PRE_POLY:56
theorem Th61: :: PRE_POLY:57
theorem Th62: :: PRE_POLY:58
theorem Th63: :: PRE_POLY:59
theorem :: PRE_POLY:60
:: deftheorem Def16 defines BagOrder PRE_POLY:def 14 :
Lm1:
for n being Ordinal holds BagOrder n is_reflexive_in Bags n
Lm2:
for n being Ordinal holds BagOrder n is_antisymmetric_in Bags n
Lm3:
for n being Ordinal holds BagOrder n is_transitive_in Bags n
Lm4:
for n being Ordinal holds BagOrder n linearly_orders Bags n
:: deftheorem Def17 defines NatMinor PRE_POLY:def 15 :
theorem Th65: :: PRE_POLY:61
theorem Th66: :: PRE_POLY:62
theorem Th67: :: PRE_POLY:63
:: deftheorem Def18 defines divisors PRE_POLY:def 16 :
theorem Th68: :: PRE_POLY:64
theorem Th69: :: PRE_POLY:65
theorem Th70: :: PRE_POLY:66
theorem Th71: :: PRE_POLY:67
:: deftheorem Def19 defines decomp PRE_POLY:def 17 :
theorem Th72: :: PRE_POLY:68
theorem Th73: :: PRE_POLY:69
theorem Th74: :: PRE_POLY:70
theorem :: PRE_POLY:71
theorem :: PRE_POLY:72
theorem :: PRE_POLY:73
theorem :: PRE_POLY:74
theorem :: PRE_POLY:75