:: Properties of Relational Structures, Posets, Lattices and Maps
:: by Mariusz \.Zynel and Czes{\l}aw Byli\'nski
::
:: Received September 20, 1996
:: Copyright (c) 1996-2012 Association of Mizar Users
begin
theorem
:: YELLOW_2:1
for
L
being non
empty
RelStr
for
x
being
Element
of
L
for
X
being
Subset
of
L
holds
(
X
c=
downarrow
x
iff
X
is_<=_than
x
)
proof
end;
theorem
:: YELLOW_2:2
for
L
being non
empty
RelStr
for
x
being
Element
of
L
for
X
being
Subset
of
L
holds
(
X
c=
uparrow
x
iff
x
is_<=_than
X
)
proof
end;
theorem
:: YELLOW_2:3
for
L
being
transitive
antisymmetric
with_suprema
RelStr
for
X
,
Y
being
set
st
ex_sup_of
X
,
L
&
ex_sup_of
Y
,
L
holds
(
ex_sup_of
X
\/
Y
,
L
&
"\/"
(
(
X
\/
Y
)
,
L
)
=
(
"\/"
(
X
,
L
)
)
"\/"
(
"\/"
(
Y
,
L
)
)
)
proof
end;
theorem
:: YELLOW_2:4
for
L
being
transitive
antisymmetric
with_infima
RelStr
for
X
,
Y
being
set
st
ex_inf_of
X
,
L
&
ex_inf_of
Y
,
L
holds
(
ex_inf_of
X
\/
Y
,
L
&
"/\"
(
(
X
\/
Y
)
,
L
)
=
(
"/\"
(
X
,
L
)
)
"/\"
(
"/\"
(
Y
,
L
)
)
)
proof
end;
begin
theorem
Th5
:
:: YELLOW_2:5
for
R
being
Relation
for
X
,
Y
being
set
st
X
c=
Y
holds
R
|_2
X
c=
R
|_2
Y
proof
end;
theorem
:: YELLOW_2:6
for
L
being
RelStr
for
S
,
T
being
full
SubRelStr
of
L
st the
carrier
of
S
c=
the
carrier
of
T
holds
the
InternalRel
of
S
c=
the
InternalRel
of
T
proof
end;
theorem
Th7
:
:: YELLOW_2:7
for
X
being
set
for
L
being non
empty
RelStr
for
S
being non
empty
SubRelStr
of
L
holds
( (
X
is
directed
Subset
of
S
implies
X
is
directed
Subset
of
L
) & (
X
is
filtered
Subset
of
S
implies
X
is
filtered
Subset
of
L
) )
proof
end;
theorem
:: YELLOW_2:8
for
L
being non
empty
RelStr
for
S
,
T
being non
empty
full
SubRelStr
of
L
st the
carrier
of
S
c=
the
carrier
of
T
holds
for
X
being
Subset
of
S
holds
(
X
is
Subset
of
T
& ( for
Y
being
Subset
of
T
st
X
=
Y
holds
( (
X
is
filtered
implies
Y
is
filtered
) & (
X
is
directed
implies
Y
is
directed
) ) ) )
proof
end;
begin
definition
let
J
be
set
;
let
L
be
RelStr
;
let
f
,
g
be
Function
of
J
, the
carrier
of
L
;
pred
f
<=
g
means
:
Def1
:
:: YELLOW_2:def 1
for
j
being
set
st
j
in
J
holds
ex
a
,
b
being
Element
of
L
st
(
a
=
f
.
j
&
b
=
g
.
j
&
a
<=
b
);
end;
::
deftheorem
Def1
defines
<=
YELLOW_2:def 1 :
for
J
being
set
for
L
being
RelStr
for
f
,
g
being
Function
of
J
, the
carrier
of
L
holds
(
f
<=
g
iff for
j
being
set
st
j
in
J
holds
ex
a
,
b
being
Element
of
L
st
(
a
=
f
.
j
&
b
=
g
.
j
&
a
<=
b
) );
notation
let
J
be
set
;
let
L
be
RelStr
;
let
f
,
g
be
Function
of
J
, the
carrier
of
L
;
synonym
g
>=
f
for
f
<=
g
;
end;
theorem
:: YELLOW_2:9
for
L
,
M
being non
empty
RelStr
for
f
,
g
being
Function
of
L
,
M
holds
(
f
<=
g
iff for
x
being
Element
of
L
holds
f
.
x
<=
g
.
x
)
proof
end;
begin
definition
let
L
,
M
be non
empty
RelStr
;
let
f
be
Function
of
L
,
M
;
func
Image
f
->
strict
full
SubRelStr
of
M
equals
:: YELLOW_2:def 2
subrelstr
(
rng
f
)
;
correctness
coherence
subrelstr
(
rng
f
)
is
strict
full
SubRelStr
of
M
;
;
end;
::
deftheorem
defines
Image
YELLOW_2:def 2 :
for
L
,
M
being non
empty
RelStr
for
f
being
Function
of
L
,
M
holds
Image
f
=
subrelstr
(
rng
f
)
;
theorem
:: YELLOW_2:10
for
L
,
M
being non
empty
RelStr
for
f
being
Function
of
L
,
M
for
y
being
Element
of
(
Image
f
)
ex
x
being
Element
of
L
st
f
.
x
=
y
proof
end;
registration
let
L
be non
empty
RelStr
;
let
X
be non
empty
Subset
of
L
;
cluster
subrelstr
X
->
non
empty
;
coherence
not
subrelstr
X
is
empty
by
YELLOW_0:def 15
;
end;
registration
let
L
,
M
be non
empty
RelStr
;
let
f
be
Function
of
L
,
M
;
cluster
Image
f
->
non
empty
strict
full
;
coherence
not
Image
f
is
empty
proof
end;
end;
begin
theorem
:: YELLOW_2:11
for
L
being non
empty
RelStr
holds
id
L
is
monotone
proof
end;
theorem
:: YELLOW_2:12
for
L
,
M
,
N
being non
empty
RelStr
for
f
being
Function
of
L
,
M
for
g
being
Function
of
M
,
N
st
f
is
monotone
&
g
is
monotone
holds
g
*
f
is
monotone
proof
end;
theorem
:: YELLOW_2:13
for
L
,
M
being non
empty
RelStr
for
f
being
Function
of
L
,
M
for
X
being
Subset
of
L
for
x
being
Element
of
L
st
f
is
monotone
&
x
is_<=_than
X
holds
f
.
x
is_<=_than
f
.:
X
proof
end;
theorem
:: YELLOW_2:14
for
L
,
M
being non
empty
RelStr
for
f
being
Function
of
L
,
M
for
X
being
Subset
of
L
for
x
being
Element
of
L
st
f
is
monotone
&
X
is_<=_than
x
holds
f
.:
X
is_<=_than
f
.
x
proof
end;
theorem
:: YELLOW_2:15
for
S
,
T
being non
empty
RelStr
for
f
being
Function
of
S
,
T
for
X
being
directed
Subset
of
S
st
f
is
monotone
holds
f
.:
X
is
directed
proof
end;
theorem
Th16
:
:: YELLOW_2:16
for
L
being
with_suprema
Poset
for
f
being
Function
of
L
,
L
st
f
is
directed-sups-preserving
holds
f
is
monotone
proof
end;
theorem
:: YELLOW_2:17
for
L
being
with_infima
Poset
for
f
being
Function
of
L
,
L
st
f
is
filtered-infs-preserving
holds
f
is
monotone
proof
end;
begin
theorem
:: YELLOW_2:18
for
S
being non
empty
1-sorted
for
f
being
Function
of
S
,
S
st
f
is
idempotent
holds
for
x
being
Element
of
S
holds
f
.
(
f
.
x
)
=
f
.
x
proof
end;
theorem
Th19
:
:: YELLOW_2:19
for
S
being non
empty
1-sorted
for
f
being
Function
of
S
,
S
st
f
is
idempotent
holds
rng
f
=
{
x
where
x
is
Element
of
S
:
x
=
f
.
x
}
proof
end;
theorem
Th20
:
:: YELLOW_2:20
for
X
being
set
for
S
being non
empty
1-sorted
for
f
being
Function
of
S
,
S
st
f
is
idempotent
&
X
c=
rng
f
holds
f
.:
X
=
X
proof
end;
theorem
:: YELLOW_2:21
for
L
being non
empty
RelStr
holds
id
L
is
idempotent
proof
end;
begin
theorem
Th22
:
:: YELLOW_2:22
for
X
being
set
for
L
being
complete
LATTICE
for
a
being
Element
of
L
st
a
in
X
holds
(
a
<=
"\/"
(
X
,
L
) &
"/\"
(
X
,
L
)
<=
a
)
proof
end;
theorem
Th23
:
:: YELLOW_2:23
for
L
being non
empty
RelStr
holds
( ( for
X
being
set
holds
ex_sup_of
X
,
L
) iff for
Y
being
set
holds
ex_inf_of
Y
,
L
)
proof
end;
theorem
Th24
:
:: YELLOW_2:24
for
L
being non
empty
RelStr
st ( for
X
being
set
holds
ex_sup_of
X
,
L
) holds
L
is
complete
proof
end;
theorem
Th25
:
:: YELLOW_2:25
for
L
being non
empty
RelStr
st ( for
X
being
set
holds
ex_inf_of
X
,
L
) holds
L
is
complete
proof
end;
theorem
Th26
:
:: YELLOW_2:26
for
L
being non
empty
RelStr
st ( for
A
being
Subset
of
L
holds
ex_inf_of
A
,
L
) holds
for
X
being
set
holds
(
ex_inf_of
X
,
L
&
"/\"
(
X
,
L
)
=
"/\"
(
(
X
/\
the
carrier
of
L
)
,
L
) )
proof
end;
theorem
:: YELLOW_2:27
for
L
being non
empty
RelStr
st ( for
A
being
Subset
of
L
holds
ex_sup_of
A
,
L
) holds
for
X
being
set
holds
(
ex_sup_of
X
,
L
&
"\/"
(
X
,
L
)
=
"\/"
(
(
X
/\
the
carrier
of
L
)
,
L
) )
proof
end;
theorem
Th28
:
:: YELLOW_2:28
for
L
being non
empty
RelStr
st ( for
A
being
Subset
of
L
holds
ex_inf_of
A
,
L
) holds
L
is
complete
proof
end;
registration
cluster
non
empty
reflexive
transitive
antisymmetric
upper-bounded
up-complete
/\-complete
->
non
empty
complete
for
RelStr
;
correctness
coherence
for
b
1
being non
empty
Poset
st
b
1
is
up-complete
&
b
1
is
/\-complete
&
b
1
is
upper-bounded
holds
b
1
is
complete
;
;
end;
theorem
Th29
:
:: YELLOW_2:29
for
L
being
complete
LATTICE
for
f
being
Function
of
L
,
L
st
f
is
monotone
holds
for
M
being
Subset
of
L
st
M
=
{
x
where
x
is
Element
of
L
:
x
=
f
.
x
}
holds
subrelstr
M
is
complete
LATTICE
proof
end;
theorem
Th30
:
:: YELLOW_2:30
for
L
being
complete
LATTICE
for
S
being non
empty
full
infs-inheriting
SubRelStr
of
L
holds
S
is
complete
LATTICE
proof
end;
theorem
Th31
:
:: YELLOW_2:31
for
L
being
complete
LATTICE
for
S
being non
empty
full
sups-inheriting
SubRelStr
of
L
holds
S
is
complete
LATTICE
proof
end;
theorem
Th32
:
:: YELLOW_2:32
for
L
being
complete
LATTICE
for
M
being non
empty
RelStr
for
f
being
Function
of
L
,
M
st
f
is
sups-preserving
holds
Image
f
is
sups-inheriting
proof
end;
theorem
Th33
:
:: YELLOW_2:33
for
L
being
complete
LATTICE
for
M
being non
empty
RelStr
for
f
being
Function
of
L
,
M
st
f
is
infs-preserving
holds
Image
f
is
infs-inheriting
proof
end;
theorem
:: YELLOW_2:34
for
L
,
M
being
complete
LATTICE
for
f
being
Function
of
L
,
M
st (
f
is
sups-preserving
or
f
is
infs-preserving
) holds
Image
f
is
complete
LATTICE
proof
end;
theorem
:: YELLOW_2:35
for
L
being
complete
LATTICE
for
f
being
Function
of
L
,
L
st
f
is
idempotent
&
f
is
directed-sups-preserving
holds
(
Image
f
is
directed-sups-inheriting
&
Image
f
is
complete
LATTICE
)
proof
end;
begin
theorem
Th36
:
:: YELLOW_2:36
for
L
being
RelStr
for
F
being
Subset-Family
of
L
st ( for
X
being
Subset
of
L
st
X
in
F
holds
X
is
lower
) holds
meet
F
is
lower
Subset
of
L
proof
end;
theorem
:: YELLOW_2:37
for
L
being
RelStr
for
F
being
Subset-Family
of
L
st ( for
X
being
Subset
of
L
st
X
in
F
holds
X
is
upper
) holds
meet
F
is
upper
Subset
of
L
proof
end;
theorem
Th38
:
:: YELLOW_2:38
for
L
being
antisymmetric
with_suprema
RelStr
for
F
being
Subset-Family
of
L
st ( for
X
being
Subset
of
L
st
X
in
F
holds
(
X
is
lower
&
X
is
directed
) ) holds
meet
F
is
directed
Subset
of
L
proof
end;
theorem
:: YELLOW_2:39
for
L
being
antisymmetric
with_infima
RelStr
for
F
being
Subset-Family
of
L
st ( for
X
being
Subset
of
L
st
X
in
F
holds
(
X
is
upper
&
X
is
filtered
) ) holds
meet
F
is
filtered
Subset
of
L
proof
end;
theorem
Th40
:
:: YELLOW_2:40
for
L
being
with_infima
Poset
for
I
,
J
being
Ideal
of
L
holds
I
/\
J
is
Ideal
of
L
proof
end;
registration
let
L
be non
empty
reflexive
transitive
RelStr
;
cluster
Ids
L
->
non
empty
;
correctness
coherence
not
Ids
L
is
empty
;
proof
end;
end;
theorem
Th41
:
:: YELLOW_2:41
for
x
being
set
for
L
being non
empty
reflexive
transitive
RelStr
holds
(
x
is
Element
of
(
InclPoset
(
Ids
L
)
)
iff
x
is
Ideal
of
L
)
proof
end;
theorem
Th42
:
:: YELLOW_2:42
for
x
being
set
for
L
being non
empty
reflexive
transitive
RelStr
for
I
being
Element
of
(
InclPoset
(
Ids
L
)
)
st
x
in
I
holds
x
is
Element
of
L
proof
end;
theorem
:: YELLOW_2:43
for
L
being
with_infima
Poset
for
x
,
y
being
Element
of
(
InclPoset
(
Ids
L
)
)
holds
x
"/\"
y
=
x
/\
y
proof
end;
registration
let
L
be
with_infima
Poset
;
cluster
InclPoset
(
Ids
L
)
->
with_infima
;
correctness
coherence
InclPoset
(
Ids
L
)
is
with_infima
;
proof
end;
end;
theorem
Th44
:
:: YELLOW_2:44
for
L
being
with_suprema
Poset
for
x
,
y
being
Element
of
(
InclPoset
(
Ids
L
)
)
ex
Z
being
Subset
of
L
st
(
Z
=
{
z
where
z
is
Element
of
L
: (
z
in
x
or
z
in
y
or ex
a
,
b
being
Element
of
L
st
(
a
in
x
&
b
in
y
&
z
=
a
"\/"
b
) )
}
&
ex_sup_of
{
x
,
y
}
,
InclPoset
(
Ids
L
)
&
x
"\/"
y
=
downarrow
Z
)
proof
end;
registration
let
L
be
with_suprema
Poset
;
cluster
InclPoset
(
Ids
L
)
->
with_suprema
;
correctness
coherence
InclPoset
(
Ids
L
)
is
with_suprema
;
proof
end;
end;
theorem
Th45
:
:: YELLOW_2:45
for
L
being
lower-bounded
sup-Semilattice
for
X
being non
empty
Subset
of
(
Ids
L
)
holds
meet
X
is
Ideal
of
L
proof
end;
theorem
Th46
:
:: YELLOW_2:46
for
L
being
lower-bounded
sup-Semilattice
for
A
being non
empty
Subset
of
(
InclPoset
(
Ids
L
)
)
holds
(
ex_inf_of
A
,
InclPoset
(
Ids
L
)
&
inf
A
=
meet
A
)
proof
end;
theorem
Th47
:
:: YELLOW_2:47
for
L
being
with_suprema
Poset
holds
(
ex_inf_of
{}
,
InclPoset
(
Ids
L
)
&
"/\"
(
{}
,
(
InclPoset
(
Ids
L
)
)
)
=
[#]
L
)
proof
end;
theorem
Th48
:
:: YELLOW_2:48
for
L
being
lower-bounded
sup-Semilattice
holds
InclPoset
(
Ids
L
)
is
complete
proof
end;
registration
let
L
be
lower-bounded
sup-Semilattice
;
cluster
InclPoset
(
Ids
L
)
->
complete
;
correctness
coherence
InclPoset
(
Ids
L
)
is
complete
;
by
Th48
;
end;
begin
definition
let
L
be non
empty
Poset
;
func
SupMap
L
->
Function
of
(
InclPoset
(
Ids
L
)
)
,
L
means
:
Def3
:
:: YELLOW_2:def 3
for
I
being
Ideal
of
L
holds
it
.
I
=
sup
I
;
existence
ex
b
1
being
Function
of
(
InclPoset
(
Ids
L
)
)
,
L
st
for
I
being
Ideal
of
L
holds
b
1
.
I
=
sup
I
proof
end;
uniqueness
for
b
1
,
b
2
being
Function
of
(
InclPoset
(
Ids
L
)
)
,
L
st ( for
I
being
Ideal
of
L
holds
b
1
.
I
=
sup
I
) & ( for
I
being
Ideal
of
L
holds
b
2
.
I
=
sup
I
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def3
defines
SupMap
YELLOW_2:def 3 :
for
L
being non
empty
Poset
for
b
2
being
Function
of
(
InclPoset
(
Ids
L
)
)
,
L
holds
(
b
2
=
SupMap
L
iff for
I
being
Ideal
of
L
holds
b
2
.
I
=
sup
I
);
theorem
Th49
:
:: YELLOW_2:49
for
L
being non
empty
Poset
holds
(
dom
(
SupMap
L
)
=
Ids
L
&
rng
(
SupMap
L
)
is
Subset
of
L
)
proof
end;
theorem
:: YELLOW_2:50
for
x
being
set
for
L
being non
empty
Poset
holds
(
x
in
dom
(
SupMap
L
)
iff
x
is
Ideal
of
L
)
proof
end;
theorem
Th51
:
:: YELLOW_2:51
for
L
being non
empty
up-complete
Poset
holds
SupMap
L
is
monotone
proof
end;
registration
let
L
be non
empty
up-complete
Poset
;
cluster
SupMap
L
->
monotone
;
correctness
coherence
SupMap
L
is
monotone
;
by
Th51
;
end;
definition
let
L
be non
empty
Poset
;
func
IdsMap
L
->
Function
of
L
,
(
InclPoset
(
Ids
L
)
)
means
:
Def4
:
:: YELLOW_2:def 4
for
x
being
Element
of
L
holds
it
.
x
=
downarrow
x
;
existence
ex
b
1
being
Function
of
L
,
(
InclPoset
(
Ids
L
)
)
st
for
x
being
Element
of
L
holds
b
1
.
x
=
downarrow
x
proof
end;
uniqueness
for
b
1
,
b
2
being
Function
of
L
,
(
InclPoset
(
Ids
L
)
)
st ( for
x
being
Element
of
L
holds
b
1
.
x
=
downarrow
x
) & ( for
x
being
Element
of
L
holds
b
2
.
x
=
downarrow
x
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def4
defines
IdsMap
YELLOW_2:def 4 :
for
L
being non
empty
Poset
for
b
2
being
Function
of
L
,
(
InclPoset
(
Ids
L
)
)
holds
(
b
2
=
IdsMap
L
iff for
x
being
Element
of
L
holds
b
2
.
x
=
downarrow
x
);
theorem
Th52
:
:: YELLOW_2:52
for
L
being non
empty
Poset
holds
IdsMap
L
is
monotone
proof
end;
registration
let
L
be non
empty
Poset
;
cluster
IdsMap
L
->
monotone
;
correctness
coherence
IdsMap
L
is
monotone
;
by
Th52
;
end;
begin
definition
let
L
be non
empty
RelStr
;
let
F
be
Relation
;
func
\\/
(
F
,
L
)
->
Element
of
L
equals
:: YELLOW_2:def 5
"\/"
(
(
rng
F
)
,
L
);
coherence
"\/"
(
(
rng
F
)
,
L
) is
Element
of
L
;
func
//\
(
F
,
L
)
->
Element
of
L
equals
:: YELLOW_2:def 6
"/\"
(
(
rng
F
)
,
L
);
coherence
"/\"
(
(
rng
F
)
,
L
) is
Element
of
L
;
end;
::
deftheorem
defines
\\/
YELLOW_2:def 5 :
for
L
being non
empty
RelStr
for
F
being
Relation
holds
\\/
(
F
,
L
)
=
"\/"
(
(
rng
F
)
,
L
);
::
deftheorem
defines
//\
YELLOW_2:def 6 :
for
L
being non
empty
RelStr
for
F
being
Relation
holds
//\
(
F
,
L
)
=
"/\"
(
(
rng
F
)
,
L
);
notation
let
J
be
set
;
let
L
be non
empty
RelStr
;
let
F
be
Function
of
J
, the
carrier
of
L
;
synonym
Sup
F
for
\\/
(
L
,
J
);
synonym
Inf
F
for
//\
(
L
,
J
);
end;
theorem
:: YELLOW_2:53
for
L
being
complete
LATTICE
for
J
being non
empty
set
for
j
being
Element
of
J
for
F
being
Function
of
J
, the
carrier
of
L
holds
(
F
.
j
<=
Sup
&
Inf
<=
F
.
j
)
proof
end;
theorem
:: YELLOW_2:54
for
L
being
complete
LATTICE
for
a
being
Element
of
L
for
J
being non
empty
set
for
F
being
Function
of
J
, the
carrier
of
L
st ( for
j
being
Element
of
J
holds
F
.
j
<=
a
) holds
Sup
<=
a
proof
end;
theorem
:: YELLOW_2:55
for
L
being
complete
LATTICE
for
a
being
Element
of
L
for
J
being non
empty
set
for
F
being
Function
of
J
, the
carrier
of
L
st ( for
j
being
Element
of
J
holds
a
<=
F
.
j
) holds
a
<=
Inf
proof
end;