:: Lim-inf Convergence
:: by Bart{\l}omiej Skorulski
::
:: Received January 6, 2000
:: Copyright (c) 2000-2012 Association of Mizar Users
begin
theorem
Th1
:
:: WAYBEL28:1
for
L
being
complete
LATTICE
for
N
being
net
of
L
holds
inf
N
<=
lim_inf
N
proof
end;
theorem
:: WAYBEL28:2
for
L
being
complete
LATTICE
for
N
being
net
of
L
for
x
being
Element
of
L
st ( for
M
being
subnet
of
N
holds
x
=
lim_inf
M
) holds
(
x
=
lim_inf
N
& ( for
M
being
subnet
of
N
holds
x
>=
inf
M
) )
proof
end;
theorem
Th3
:
:: WAYBEL28:3
for
L
being
complete
LATTICE
for
N
being
net
of
L
for
x
being
Element
of
L
st
N
in
NetUniv
L
& ( for
M
being
subnet
of
N
st
M
in
NetUniv
L
holds
x
=
lim_inf
M
) holds
(
x
=
lim_inf
N
& ( for
M
being
subnet
of
N
st
M
in
NetUniv
L
holds
x
>=
inf
M
) )
proof
end;
definition
let
N
be non
empty
RelStr
;
let
f
be
Function
of
N
,
N
;
attr
f
is
greater_or_equal_to_id
means
:
Def1
:
:: WAYBEL28:def 1
for
j
being
Element
of
N
holds
j
<=
f
.
j
;
end;
::
deftheorem
Def1
defines
greater_or_equal_to_id
WAYBEL28:def 1 :
for
N
being non
empty
RelStr
for
f
being
Function
of
N
,
N
holds
(
f
is
greater_or_equal_to_id
iff for
j
being
Element
of
N
holds
j
<=
f
.
j
);
theorem
Th4
:
:: WAYBEL28:4
for
N
being non
empty
reflexive
RelStr
holds
id
N
is
greater_or_equal_to_id
proof
end;
theorem
Th5
:
:: WAYBEL28:5
for
N
being non
empty
directed
RelStr
for
x
,
y
being
Element
of
N
ex
z
being
Element
of
N
st
(
x
<=
z
&
y
<=
z
)
proof
end;
registration
let
N
be non
empty
directed
RelStr
;
cluster
non
empty
Relation-like
the
carrier
of
N
-defined
the
carrier
of
N
-valued
Function-like
V34
( the
carrier
of
N
)
V35
( the
carrier
of
N
, the
carrier
of
N
)
greater_or_equal_to_id
for
Element
of
bool
[:
the
carrier
of
N
, the
carrier
of
N
:]
;
existence
ex
b
1
being
Function
of
N
,
N
st
b
1
is
greater_or_equal_to_id
proof
end;
end;
registration
let
N
be non
empty
reflexive
RelStr
;
cluster
non
empty
Relation-like
the
carrier
of
N
-defined
the
carrier
of
N
-valued
Function-like
V34
( the
carrier
of
N
)
V35
( the
carrier
of
N
, the
carrier
of
N
)
greater_or_equal_to_id
for
Element
of
bool
[:
the
carrier
of
N
, the
carrier
of
N
:]
;
existence
ex
b
1
being
Function
of
N
,
N
st
b
1
is
greater_or_equal_to_id
proof
end;
end;
definition
let
L
be non
empty
1-sorted
;
let
N
be non
empty
NetStr
over
L
;
let
f
be
Function
of
N
,
N
;
func
N
*
f
->
non
empty
strict
NetStr
over
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
b
1
being non
empty
strict
NetStr
over
L
st
(
RelStr
(# the
carrier
of
b
1
, the
InternalRel
of
b
1
#)
=
RelStr
(# the
carrier
of
N
, the
InternalRel
of
N
#) & the
mapping
of
b
1
=
the
mapping
of
N
*
f
)
proof
end;
uniqueness
for
b
1
,
b
2
being non
empty
strict
NetStr
over
L
st
RelStr
(# the
carrier
of
b
1
, the
InternalRel
of
b
1
#)
=
RelStr
(# the
carrier
of
N
, the
InternalRel
of
N
#) & the
mapping
of
b
1
=
the
mapping
of
N
*
f
&
RelStr
(# the
carrier
of
b
2
, the
InternalRel
of
b
2
#)
=
RelStr
(# the
carrier
of
N
, the
InternalRel
of
N
#) & the
mapping
of
b
2
=
the
mapping
of
N
*
f
holds
b
1
=
b
2
;
end;
::
deftheorem
Def2
defines
*
WAYBEL28:def 2 :
for
L
being non
empty
1-sorted
for
N
being non
empty
NetStr
over
L
for
f
being
Function
of
N
,
N
for
b
4
being non
empty
strict
NetStr
over
L
holds
(
b
4
=
N
*
f
iff (
RelStr
(# the
carrier
of
b
4
, the
InternalRel
of
b
4
#)
=
RelStr
(# the
carrier
of
N
, the
InternalRel
of
N
#) & the
mapping
of
b
4
=
the
mapping
of
N
*
f
) );
theorem
Th6
:
:: WAYBEL28:6
for
L
being non
empty
1-sorted
for
N
being non
empty
NetStr
over
L
for
f
being
Function
of
N
,
N
holds the
carrier
of
(
N
*
f
)
=
the
carrier
of
N
proof
end;
theorem
Th7
:
:: WAYBEL28:7
for
L
being non
empty
1-sorted
for
N
being non
empty
NetStr
over
L
for
f
being
Function
of
N
,
N
holds
N
*
f
=
NetStr
(# the
carrier
of
N
, the
InternalRel
of
N
,
(
the
mapping
of
N
*
f
)
#)
proof
end;
theorem
Th8
:
:: WAYBEL28:8
for
L
being non
empty
1-sorted
for
N
being non
empty
transitive
directed
RelStr
for
f
being
Function
of the
carrier
of
N
, the
carrier
of
L
holds
NetStr
(# the
carrier
of
N
, the
InternalRel
of
N
,
f
#) is
net
of
L
proof
end;
registration
let
L
be non
empty
1-sorted
;
let
N
be non
empty
transitive
directed
RelStr
;
let
f
be
Function
of the
carrier
of
N
, the
carrier
of
L
;
cluster
NetStr
(# the
carrier
of
N
, the
InternalRel
of
N
,
f
#)
->
non
empty
transitive
directed
;
correctness
coherence
(
NetStr
(# the
carrier
of
N
, the
InternalRel
of
N
,
f
#) is
transitive
&
NetStr
(# the
carrier
of
N
, the
InternalRel
of
N
,
f
#) is
directed
& not
NetStr
(# the
carrier
of
N
, the
InternalRel
of
N
,
f
#) is
empty
)
;
by
Th8
;
end;
theorem
Th9
:
:: WAYBEL28:9
for
L
being non
empty
1-sorted
for
N
being
net
of
L
for
p
being
Function
of
N
,
N
holds
N
*
p
is
net
of
L
proof
end;
registration
let
L
be non
empty
1-sorted
;
let
N
be
net
of
L
;
let
p
be
Function
of
N
,
N
;
cluster
N
*
p
->
non
empty
transitive
strict
directed
;
correctness
coherence
(
N
*
p
is
transitive
&
N
*
p
is
directed
)
;
by
Th9
;
end;
theorem
Th10
:
:: WAYBEL28:10
for
L
being non
empty
1-sorted
for
N
being
net
of
L
for
p
being
Function
of
N
,
N
st
N
in
NetUniv
L
holds
N
*
p
in
NetUniv
L
proof
end;
theorem
:: WAYBEL28:11
for
L
being non
empty
1-sorted
for
N
,
M
being
net
of
L
st
NetStr
(# the
carrier
of
N
, the
InternalRel
of
N
, the
mapping
of
N
#)
=
NetStr
(# the
carrier
of
M
, the
InternalRel
of
M
, the
mapping
of
M
#) holds
M
is
subnet
of
N
proof
end;
theorem
Th12
:
:: WAYBEL28:12
for
L
being non
empty
1-sorted
for
N
being
net
of
L
for
p
being
greater_or_equal_to_id
Function
of
N
,
N
holds
N
*
p
is
subnet
of
N
proof
end;
definition
let
L
be non
empty
1-sorted
;
let
N
be
net
of
L
;
let
p
be
greater_or_equal_to_id
Function
of
N
,
N
;
:: original:
*
redefine
func
N
*
p
->
strict
subnet
of
N
;
correctness
coherence
N
*
p
is
strict
subnet
of
N
;
by
Th12
;
end;
theorem
:: WAYBEL28:13
for
L
being
complete
LATTICE
for
N
being
net
of
L
for
x
being
Element
of
L
st
N
in
NetUniv
L
&
x
=
lim_inf
N
& ( for
M
being
subnet
of
N
st
M
in
NetUniv
L
holds
x
>=
inf
M
) holds
(
x
=
lim_inf
N
& ( for
p
being
greater_or_equal_to_id
Function
of
N
,
N
holds
x
>=
inf
(
N
*
p
)
) )
by
Th10
;
theorem
Th14
:
:: WAYBEL28:14
for
L
being
complete
LATTICE
for
N
being
net
of
L
for
x
being
Element
of
L
st
x
=
lim_inf
N
& ( for
p
being
greater_or_equal_to_id
Function
of
N
,
N
holds
x
>=
inf
(
N
*
p
)
) holds
for
M
being
subnet
of
N
holds
x
=
lim_inf
M
proof
end;
definition
let
L
be non
empty
RelStr
;
func
lim_inf-Convergence
L
->
Convergence-Class
of
L
means
:
Def3
:
:: WAYBEL28:def 3
for
N
being
net
of
L
st
N
in
NetUniv
L
holds
for
x
being
Element
of
L
holds
(
[
N
,
x
]
in
it
iff for
M
being
subnet
of
N
holds
x
=
lim_inf
M
);
existence
ex
b
1
being
Convergence-Class
of
L
st
for
N
being
net
of
L
st
N
in
NetUniv
L
holds
for
x
being
Element
of
L
holds
(
[
N
,
x
]
in
b
1
iff for
M
being
subnet
of
N
holds
x
=
lim_inf
M
)
proof
end;
uniqueness
for
b
1
,
b
2
being
Convergence-Class
of
L
st ( for
N
being
net
of
L
st
N
in
NetUniv
L
holds
for
x
being
Element
of
L
holds
(
[
N
,
x
]
in
b
1
iff for
M
being
subnet
of
N
holds
x
=
lim_inf
M
) ) & ( for
N
being
net
of
L
st
N
in
NetUniv
L
holds
for
x
being
Element
of
L
holds
(
[
N
,
x
]
in
b
2
iff for
M
being
subnet
of
N
holds
x
=
lim_inf
M
) ) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def3
defines
lim_inf-Convergence
WAYBEL28:def 3 :
for
L
being non
empty
RelStr
for
b
2
being
Convergence-Class
of
L
holds
(
b
2
=
lim_inf-Convergence
L
iff for
N
being
net
of
L
st
N
in
NetUniv
L
holds
for
x
being
Element
of
L
holds
(
[
N
,
x
]
in
b
2
iff for
M
being
subnet
of
N
holds
x
=
lim_inf
M
) );
theorem
:: WAYBEL28:15
for
L
being
complete
LATTICE
for
N
being
net
of
L
for
x
being
Element
of
L
st
N
in
NetUniv
L
holds
(
[
N
,
x
]
in
lim_inf-Convergence
L
iff for
M
being
subnet
of
N
st
M
in
NetUniv
L
holds
x
=
lim_inf
M
)
proof
end;
theorem
Th16
:
:: WAYBEL28:16
for
L
being non
empty
RelStr
for
N
being
constant
net
of
L
for
M
being
subnet
of
N
holds
(
M
is
constant
&
the_value_of
N
=
the_value_of
M
)
proof
end;
definition
let
L
be non
empty
RelStr
;
func
xi
L
->
Subset-Family
of
L
equals
:: WAYBEL28:def 4
the
topology
of
(
ConvergenceSpace
(
lim_inf-Convergence
L
)
)
;
correctness
coherence
the
topology
of
(
ConvergenceSpace
(
lim_inf-Convergence
L
)
)
is
Subset-Family
of
L
;
by
YELLOW_6:def 24
;
end;
::
deftheorem
defines
xi
WAYBEL28:def 4 :
for
L
being non
empty
RelStr
holds
xi
L
=
the
topology
of
(
ConvergenceSpace
(
lim_inf-Convergence
L
)
)
;
theorem
:: WAYBEL28:17
for
L
being
complete
LATTICE
holds
lim_inf-Convergence
L
is
(CONSTANTS)
proof
end;
theorem
:: WAYBEL28:18
for
L
being non
empty
RelStr
holds
lim_inf-Convergence
L
is
(SUBNETS)
proof
end;
theorem
:: WAYBEL28:19
for
L
being
continuous
complete
LATTICE
holds
lim_inf-Convergence
L
is
(DIVERGENCE)
proof
end;
theorem
:: WAYBEL28:20
for
L
being non
empty
RelStr
for
N
,
x
being
set
st
[
N
,
x
]
in
lim_inf-Convergence
L
holds
N
in
NetUniv
L
proof
end;
theorem
Th21
:
:: WAYBEL28:21
for
L
being non
empty
1-sorted
for
C1
,
C2
being
Convergence-Class
of
L
st
C1
c=
C2
holds
the
topology
of
(
ConvergenceSpace
C2
)
c=
the
topology
of
(
ConvergenceSpace
C1
)
proof
end;
theorem
Th22
:
:: WAYBEL28:22
for
L
being non
empty
reflexive
RelStr
holds
lim_inf-Convergence
L
c=
Scott-Convergence
L
proof
end;
theorem
Th23
:
:: WAYBEL28:23
for
X
,
Y
being
set
st
X
c=
Y
holds
X
in
the_universe_of
Y
proof
end;
theorem
Th24
:
:: WAYBEL28:24
for
L
being non
empty
reflexive
transitive
RelStr
for
D
being non
empty
directed
Subset
of
L
holds
Net-Str
D
in
NetUniv
L
proof
end;
theorem
Th25
:
:: WAYBEL28:25
for
L
being
complete
LATTICE
for
D
being non
empty
directed
Subset
of
L
for
M
being
subnet
of
Net-Str
D
holds
lim_inf
M
=
sup
D
proof
end;
theorem
Th26
:
:: WAYBEL28:26
for
L
being non
empty
complete
LATTICE
for
D
being non
empty
directed
Subset
of
L
holds
[
(
Net-Str
D
)
,
(
sup
D
)
]
in
lim_inf-Convergence
L
proof
end;
theorem
Th27
:
:: WAYBEL28:27
for
L
being
complete
LATTICE
for
U1
being
Subset
of
L
st
U1
in
xi
L
holds
U1
is
property(S)
proof
end;
theorem
Th28
:
:: WAYBEL28:28
for
L
being non
empty
reflexive
RelStr
for
A
being
Subset
of
L
st
A
in
sigma
L
holds
A
in
xi
L
proof
end;
theorem
Th29
:
:: WAYBEL28:29
for
L
being
complete
LATTICE
for
A
being
Subset
of
L
st
A
is
upper
&
A
in
xi
L
holds
A
in
sigma
L
proof
end;
theorem
:: WAYBEL28:30
for
L
being
complete
LATTICE
for
A
being
Subset
of
L
st
A
is
lower
holds
(
A
`
in
xi
L
iff
A
is
closed_under_directed_sups
)
proof
end;