:: Lim-inf Convergence
:: by Bart{\l}omiej Skorulski
::
:: Received January 6, 2000
:: Copyright (c) 2000 Association of Mizar Users
theorem Th1: :: WAYBEL28:1
theorem :: WAYBEL28:2
theorem Th3: :: WAYBEL28:3
:: deftheorem Def1 defines greater_or_equal_to_id WAYBEL28:def 1 :
theorem Th4: :: WAYBEL28:4
theorem Th5: :: WAYBEL28:5
theorem Th6: :: WAYBEL28:6
definition
let L be non
empty 1-sorted ;
let N be non
empty NetStr of
L;
let f be
Function of
N,
N;
func N * f -> non
empty strict NetStr of
L means :
Def2:
:: WAYBEL28:def 2
(
RelStr(# the
carrier of
it,the
InternalRel of
it #)
= RelStr(# the
carrier of
N,the
InternalRel of
N #) & the
mapping of
it = the
mapping of
N * f );
existence
ex b1 being non empty strict NetStr of L st
( RelStr(# the carrier of b1,the InternalRel of b1 #) = RelStr(# the carrier of N,the InternalRel of N #) & the mapping of b1 = the mapping of N * f )
uniqueness
for b1, b2 being non empty strict NetStr of L st RelStr(# the carrier of b1,the InternalRel of b1 #) = RelStr(# the carrier of N,the InternalRel of N #) & the mapping of b1 = the mapping of N * f & RelStr(# the carrier of b2,the InternalRel of b2 #) = RelStr(# the carrier of N,the InternalRel of N #) & the mapping of b2 = the mapping of N * f holds
b1 = b2
;
end;
:: deftheorem Def2 defines * WAYBEL28:def 2 :
theorem Th7: :: WAYBEL28:7
theorem Th8: :: WAYBEL28:8
theorem Th9: :: WAYBEL28:9
theorem Th10: :: WAYBEL28:10
theorem Th11: :: WAYBEL28:11
theorem :: WAYBEL28:12
theorem Th13: :: WAYBEL28:13
theorem :: WAYBEL28:14
theorem Th15: :: WAYBEL28:15
:: deftheorem Def3 defines lim_inf-Convergence WAYBEL28:def 3 :
theorem :: WAYBEL28:16
theorem Th17: :: WAYBEL28:17
:: deftheorem defines xi WAYBEL28:def 4 :
theorem :: WAYBEL28:18
theorem :: WAYBEL28:19
theorem :: WAYBEL28:20
theorem :: WAYBEL28:21
theorem Th22: :: WAYBEL28:22
theorem Th23: :: WAYBEL28:23
theorem Th24: :: WAYBEL28:24
theorem Th25: :: WAYBEL28:25
theorem Th26: :: WAYBEL28:26
theorem Th27: :: WAYBEL28:27
theorem Th28: :: WAYBEL28:28
theorem Th29: :: WAYBEL28:29
theorem Th30: :: WAYBEL28:30
theorem :: WAYBEL28:31