poset_2.miz
begin
reserve a,Z1,Z2,Z3 for
set,
x,y,z for
object,
k for
Nat;
LemSUM01: a
in ((Z1
\/ Z2)
\/ Z3) iff a
in Z1 or a
in Z2 or a
in Z3
proof
a
in ((Z1
\/ Z2)
\/ Z3) iff a
in (Z1
\/ Z2) or a
in Z3 by
XBOOLE_0:def 3;
hence thesis by
XBOOLE_0:def 3;
end;
LemMin01: for S be non
empty
RelStr, a be
Element of S holds a
is_<=_than the
carrier of S iff for x be
Element of S holds a
<= x;
theorem ::
POSET_2:1
ThMin02: for P be
lower-bounded non
empty
Poset, p be
Element of P st p
is_<=_than the
carrier of P holds p
= (
Bottom P)
proof
let P be
lower-bounded non
empty
Poset;
let p be
Element of P;
assume
A1: p
is_<=_than the
carrier of P;
A2:
ex_sup_of (
{} ,P) by
YELLOW_0: 42;
A3:
{}
is_<=_than p;
for a be
Element of P st
{}
is_<=_than a holds p
<= a by
A1;
hence thesis by
A2,
A3,
YELLOW_0:def 9;
end;
theorem ::
POSET_2:2
Thsup01: for P be
chain-complete non
empty
Poset, L be non
empty
Chain of P holds for p be
Element of P st p
in L holds p
<= (
sup L)
proof
let P be
chain-complete non
empty
Poset;
let L be non
empty
Chain of P;
let p be
Element of P;
assume
A1: p
in L;
A2:
ex_sup_of (L,P) by
POSET_1:def 1;
reconsider x = (
sup L) as
Element of P;
L
is_<=_than x by
YELLOW_0:def 9,
A2;
hence thesis by
A1;
end;
theorem ::
POSET_2:3
Thsup02: for P be
chain-complete non
empty
Poset, L be non
empty
Chain of P holds for p1 be
Element of P st (for p be
Element of P st p
in L holds p
<= p1) holds (
sup L)
<= p1
proof
let P be
chain-complete non
empty
Poset;
let L be non
empty
Chain of P;
let p1 be
Element of P;
assume for p be
Element of P st p
in L holds p
<= p1;
then
A1: L
is_<=_than p1;
ex_sup_of (L,P) by
POSET_1:def 1;
hence thesis by
YELLOW_0:def 9,
A1;
end;
begin
theorem ::
POSET_2:4
ThProdPoset01: for P,Q be non
empty
RelStr, x be
object holds x is
Element of
[:P, Q:] iff ex p be
Element of P, q be
Element of Q st x
=
[p, q]
proof
let P,Q be non
empty
RelStr;
let x be
object;
x
in the
carrier of
[:P, Q:] iff x
in
[:the
carrier of P, the
carrier of Q:] by
YELLOW_3:def 2;
then x
in the
carrier of
[:P, Q:] iff ex p,q be
object st p
in the
carrier of P & q
in the
carrier of Q & x
=
[p, q] by
ZFMISC_1:def 2;
hence thesis;
end;
definition
let P,Q be non
empty
Poset;
let L be non
empty
Chain of
[:P, Q:];
:: original:
proj1
redefine
func
proj1 L -> non
empty
Chain of P ;
correctness
proof
set R = the
InternalRel of
[:P, Q:];
reconsider L as
Relation of the
carrier of P, the
carrier of Q by
YELLOW_3:def 2;
reconsider L1 = (
dom L) as
Subset of P;
reconsider L2 = (
rng L) as
Subset of Q;
set R1 = the
InternalRel of P;
x
in L1 & y
in L1 implies
[x, y]
in R1 or
[y, x]
in R1
proof
assume
B1: x
in L1 & y
in L1;
then
reconsider x, y as
Element of P;
consider q1 be
object such that
B2:
[x, q1]
in L by
XTUPLE_0:def 12,
B1;
consider q2 be
object such that
B3:
[y, q2]
in L by
XTUPLE_0:def 12,
B1;
q1
in L2 & q2
in L2 by
B2,
B3,
XTUPLE_0:def 13;
then
reconsider q1, q2 as
Element of Q;
reconsider a =
[x, q1] as
Element of
[:P, Q:];
reconsider b =
[y, q2] as
Element of
[:P, Q:];
per cases by
ORDERS_2:def 7,
RELAT_2:def 7,
B2,
B3;
suppose a
<= b;
then x
<= y by
YELLOW_3: 11;
hence thesis;
end;
suppose b
<= a;
then y
<= x by
YELLOW_3: 11;
hence thesis;
end;
end;
hence thesis by
ORDERS_2:def 7,
RELAT_2:def 7;
end;
:: original:
proj2
redefine
func
proj2 L -> non
empty
Chain of Q ;
correctness
proof
set R = the
InternalRel of
[:P, Q:];
reconsider L as
Relation of the
carrier of P, the
carrier of Q by
YELLOW_3:def 2;
reconsider L1 = (
dom L) as
Subset of P;
reconsider L2 = (
rng L) as
Subset of Q;
set R2 = the
InternalRel of Q;
x
in L2 & y
in L2 implies
[x, y]
in R2 or
[y, x]
in R2
proof
assume
B1: x
in L2 & y
in L2;
then
reconsider x, y as
Element of Q;
consider p1 be
object such that
B2:
[p1, x]
in L by
XTUPLE_0:def 13,
B1;
consider p2 be
object such that
B3:
[p2, y]
in L by
XTUPLE_0:def 13,
B1;
p1
in L1 & p2
in L1 by
B2,
B3,
XTUPLE_0:def 12;
then
reconsider p1, p2 as
Element of P;
reconsider a =
[p1, x], b =
[p2, y] as
Element of
[:P, Q:];
per cases by
ORDERS_2:def 7,
RELAT_2:def 7,
B2,
B3;
suppose a
<= b;
then x
<= y by
YELLOW_3: 11;
hence thesis;
end;
suppose b
<= a;
then y
<= x by
YELLOW_3: 11;
hence thesis;
end;
end;
hence thesis by
ORDERS_2:def 7,
RELAT_2:def 7;
end;
end
registration
let P,Q1,Q2 be non
empty
Poset;
let f1 be
monotone
Function of P, Q1;
let f2 be
monotone
Function of P, Q2;
cluster
<:f1, f2:> ->
monotone;
correctness
proof
set f =
<:f1, f2:>;
for x,y be
Element of P st x
<= y holds for a,b be
Element of
[:Q1, Q2:] st a
= (f
. x) & b
= (f
. y) holds a
<= b
proof
let x,y be
Element of P such that
B1: x
<= y;
let a,b be
Element of
[:Q1, Q2:] such that
B2: a
= (f
. x) & b
= (f
. y);
(
dom f)
= the
carrier of P by
FUNCT_2:def 1;
then
B3: a
=
[(f1
. x), (f2
. x)] & b
=
[(f1
. y), (f2
. y)] by
FUNCT_3:def 7,
B2;
(f1
. x)
<= (f1
. y) & (f2
. x)
<= (f2
. y) by
B1,
ORDERS_3:def 5;
hence thesis by
YELLOW_3: 11,
B3;
end;
hence thesis;
end;
end
LemProdPoset06: for P,Q be
chain-complete non
empty
Poset holds for L be
Chain of
[:P, Q:] st L is non
empty holds
ex_sup_of (L,
[:P, Q:])
proof
let P,Q be
chain-complete non
empty
Poset;
let L be
Chain of
[:P, Q:];
set R = the
InternalRel of
[:P, Q:];
assume L is non
empty;
then
reconsider L as non
empty
Chain of
[:P, Q:];
reconsider L1 = (
proj1 L) as non
empty
Chain of P;
reconsider L2 = (
proj2 L) as non
empty
Chain of Q;
reconsider z =
[(
sup L1), (
sup L2)] as
Element of
[:P, Q:];
a1: for x be
Element of
[:P, Q:] st x
in L holds x
<= z
proof
let x be
Element of
[:P, Q:] such that
B1: x
in L;
consider p be
Element of P, q be
Element of Q such that
B2: x
=
[p, q] by
ThProdPoset01;
p
in L1 & q
in L2 by
XTUPLE_0:def 12,
XTUPLE_0:def 13,
B1,
B2;
then p
<= (
sup L1) & q
<= (
sup L2) by
Thsup01;
hence thesis by
YELLOW_3: 11,
B2;
end;
for y be
Element of
[:P, Q:] st L
is_<=_than y holds z
<= y
proof
let y be
Element of
[:P, Q:];
consider p1 be
Element of P, q1 be
Element of Q such that
B1: y
=
[p1, q1] by
ThProdPoset01;
L
is_<=_than y implies z
<= y
proof
assume
C1: L
is_<=_than y;
C2: for p be
Element of P st p
in L1 holds p
<= p1
proof
let p be
Element of P;
assume p
in L1;
then
consider q0 be
object such that
D1:
[p, q0]
in L by
XTUPLE_0:def 12;
q0
in L2 by
D1,
XTUPLE_0:def 13;
then
reconsider q0 as
Element of Q;
reconsider b =
[p, q0] as
Element of
[:P, Q:];
b
<= y by
C1,
D1;
hence thesis by
B1,
YELLOW_3: 11;
end;
for q be
Element of Q st q
in L2 holds q
<= q1
proof
let q be
Element of Q;
assume q
in L2;
then
consider p0 be
object such that
D1:
[p0, q]
in L by
XTUPLE_0:def 13;
p0
in L1 by
D1,
XTUPLE_0:def 12;
then
reconsider p0 as
Element of P;
reconsider b =
[p0, q] as
Element of
[:P, Q:];
b
<= y by
C1,
D1;
hence thesis by
B1,
YELLOW_3: 11;
end;
then (
sup L1)
<= p1 & (
sup L2)
<= q1 by
C2,
Thsup02;
hence thesis by
YELLOW_3: 11,
B1;
end;
hence thesis;
end;
hence thesis by
a1,
YELLOW_0: 15,
LATTICE3:def 9;
end;
registration
let P,Q be
chain-complete non
empty
Poset;
cluster
[:P, Q:] ->
chain-complete;
correctness by
LemProdPoset06;
end
theorem ::
POSET_2:5
for P,Q be
chain-complete non
empty
Poset, L be non
empty
Chain of
[:P, Q:] holds (
sup L)
=
[(
sup (
proj1 L)), (
sup (
proj2 L))] by
YELLOW_3: 46,
LemProdPoset06;
registration
let P,Q1,Q2 be
strict
chain-complete non
empty
Poset;
let f1 be
continuous
Function of P, Q1;
let f2 be
continuous
Function of P, Q2;
cluster
<:f1, f2:> ->
continuous;
correctness
proof
reconsider f =
<:f1, f2:> as
monotone
Function of P,
[:Q1, Q2:] by
YELLOW_3:def 2;
for L be non
empty
Chain of P holds (f
. (
sup L))
<= (
sup (f
.: L))
proof
let L be non
empty
Chain of P;
B0: (f1
. (
sup L))
= (
sup (f1
.: L)) & (f2
. (
sup L))
= (
sup (f2
.: L)) by
POSET_1: 6;
AA: (
dom f)
= the
carrier of P by
FUNCT_2:def 1;
then
B1: (f
. (
sup L))
=
[(
sup (f1
.: L)), (
sup (f2
.: L))] by
FUNCT_3:def 7,
B0;
reconsider M = (f
.: L) as non
empty
Chain of
[:Q1, Q2:] by
POSET_1: 1;
B2: (
sup (f
.: L))
=
[(
sup (
proj1 M)), (
sup (
proj2 M))] by
YELLOW_3: 46,
LemProdPoset06;
B3: (
sup (f1
.: L))
<= (
sup (
proj1 M))
proof
reconsider M1 = (f1
.: L) as non
empty
Chain of Q1 by
POSET_1: 1;
set q1 = (
sup (
proj1 M));
for q be
Element of Q1 st q
in M1 holds q
<= q1
proof
let q be
Element of Q1;
assume q
in M1;
then
consider p be
Element of P such that
C1: p
in L & q
= (f1
. p) by
FUNCT_2: 65;
reconsider a = (f2
. p) as
Element of Q2;
(f
. p)
=
[q, a] by
C1,
FUNCT_3:def 7,
AA;
then
[q, a]
in M by
C1,
FUNCT_2: 35;
then q
in (
proj1 M) by
XTUPLE_0:def 12;
hence thesis by
Thsup01;
end;
hence thesis by
Thsup02;
end;
(
sup (f2
.: L))
<= (
sup (
proj2 M))
proof
reconsider M2 = (f2
.: L) as non
empty
Chain of Q2 by
POSET_1: 1;
set q2 = (
sup (
proj2 M));
for q be
Element of Q2 st q
in M2 holds q
<= q2
proof
let q be
Element of Q2;
assume q
in M2;
then
consider p be
Element of P such that
C1: p
in L & q
= (f2
. p) by
FUNCT_2: 65;
reconsider a = (f1
. p) as
Element of Q1;
(f
. p)
=
[a, q] by
C1,
FUNCT_3:def 7,
AA;
then
[a, q]
in M by
C1,
FUNCT_2: 35;
then q
in (
proj2 M) by
XTUPLE_0:def 13;
hence thesis by
Thsup01;
end;
hence thesis by
Thsup02;
end;
hence thesis by
B1,
B2,
B3,
YELLOW_3: 11;
end;
hence thesis by
POSET_1: 8;
end;
end
begin
definition
let IT be
RelStr;
::
POSET_2:def1
attr IT is
flat means
:
Defflat: ex a be
Element of IT st for x,y be
Element of IT holds (x
<= y iff x
= a or x
= y);
end
registration
cluster
discrete ->
reflexive for non
empty
RelStr;
coherence by
ORDERS_3: 1;
end
registration
cluster
trivial ->
flat for
discrete non
empty
RelStr;
coherence
proof
let IT be
discrete non
empty
RelStr;
assume
A: IT is
trivial;
ex a be
Element of IT st a
is_<=_than the
carrier of IT & (for x,y be
Element of IT holds (x
<= y iff x
= a or x
= y))
proof
take a = the
Element of IT;
for b be
Element of IT st b
in the
carrier of IT holds a
<= b by
A,
STRUCT_0:def 10;
hence thesis by
STRUCT_0:def 10,
A;
end;
hence thesis;
end;
end
registration
cluster
strict non
empty
flat for
Poset;
existence
proof
set A =
{
{} };
reconsider R = (
id A) as
Relation of A;
reconsider R as
Order of A;
take IT =
RelStr (# A, R #);
reconsider z =
{} as
Element of IT by
TARSKI:def 1;
ex a be
Element of IT st a
is_<=_than the
carrier of IT & (for x,y be
Element of IT holds (x
<= y iff x
= a or x
= y))
proof
b1: for x be
Element of IT holds z
<= x by
TARSKI:def 1;
for x,y be
Element of IT holds (x
<= y iff x
= z or x
= y) by
TARSKI:def 1;
hence thesis by
b1,
LemMin01;
end;
hence thesis;
end;
end
registration
cluster
flat ->
reflexive
transitive
antisymmetric for
RelStr;
correctness
proof
let S be
RelStr;
assume S is
flat;
then
consider a be
Element of S such that
A1: for x,y be
Element of S holds (x
<= y iff x
= a or x
= y);
set R = the
InternalRel of S;
set X = the
carrier of S;
R
is_reflexive_in X
proof
x
in X implies
[x, x]
in R
proof
assume x
in X;
then
reconsider x as
Element of S;
x
<= x by
A1;
hence thesis;
end;
hence thesis;
end;
hence S is
reflexive;
R
is_transitive_in X
proof
x
in X & y
in X & z
in X &
[x, y]
in R &
[y, z]
in R implies
[x, z]
in R
proof
assume
B1: x
in X & y
in X & z
in X &
[x, y]
in R &
[y, z]
in R;
then
reconsider x, y, z as
Element of S;
x
<= z
proof
x
= a or x
= y by
B1,
ORDERS_2:def 5,
A1;
hence thesis by
A1,
B1;
end;
hence thesis;
end;
hence thesis;
end;
hence S is
transitive;
R
is_antisymmetric_in X
proof
x
in X & y
in X &
[x, y]
in R &
[y, x]
in R implies x
= y
proof
assume
B1: x
in X & y
in X &
[x, y]
in R &
[y, x]
in R;
then
reconsider x, y as
Element of S;
x
= a or x
= y by
B1,
ORDERS_2:def 5,
A1;
hence thesis by
A1,
B1,
ORDERS_2:def 5;
end;
hence thesis;
end;
hence thesis;
end;
end
registration
cluster
flat ->
lower-bounded for non
empty
Poset;
coherence
proof
let P be non
empty
Poset;
assume P is
flat;
then
consider a be
Element of P such that
A1: for x,y be
Element of P holds x
<= y iff x
= a or x
= y;
take a;
thus thesis by
A1;
end;
end
reserve S for
RelStr;
reserve P,Q for non
empty
flat
Poset;
reserve p,p1,p2 for
Element of P;
reserve K for non
empty
Chain of P;
Lemflat01: p1
<= p2 iff p1
= (
Bottom P) or p1
= p2
proof
consider a be
Element of P such that
A1: for x,y be
Element of P holds (x
<= y iff x
= a or x
= y) by
Defflat;
a
= (
Bottom P)
proof
for x be
Element of P holds a
<= x by
A1;
hence thesis by
ThMin02,
LemMin01;
end;
hence thesis by
A1;
end;
theorem ::
POSET_2:6
Thflat01: for P be non
empty
flat
Poset, K be non
empty
Chain of P holds ex a be
Element of P st K
=
{a} or K
=
{(
Bottom P), a}
proof
let P be non
empty
flat
Poset, K be non
empty
Chain of P;
set z = (
Bottom P);
per cases ;
suppose ex a be
Element of K st a
<> z;
then
consider a be
Element of K such that
B1: a
<> z;
take a;
D1: x
in K implies x
= z or x
= a
proof
assume
E1: x
in K;
then
reconsider x as
Element of P;
x
<= a or a
<= x by
E1,
RELAT_2:def 7,
ORDERS_2:def 7;
hence thesis by
Lemflat01,
B1;
end;
K
=
{a} or K
=
{z, a}
proof
per cases ;
suppose
C1: z
in K;
x
= z or x
= a implies x
in K by
C1;
hence thesis by
D1,
TARSKI:def 2;
end;
suppose
C2: not z
in K;
D1: x
in K implies x
= a
proof
assume
E1: x
in K;
reconsider x as
Element of P by
E1;
x
<= a or a
<= x by
E1,
RELAT_2:def 7,
ORDERS_2:def 7;
hence thesis by
B1,
E1,
C2,
Lemflat01;
end;
for x st x
= a holds x
in K;
hence thesis by
D1,
TARSKI:def 1;
end;
end;
hence thesis;
end;
suppose
A1: not ex a be
Element of K st a
<> z;
take z;
B1: x
in K implies x
= z by
A1;
x
= z implies x
in K
proof
assume
C1: x
= z;
the
Element of K
= z by
A1;
hence thesis by
C1;
end;
hence thesis by
B1,
TARSKI:def 1;
end;
end;
Lemflat02: for K be
Chain of P st K is non
empty holds
ex_sup_of (K,P)
proof
let K be
Chain of P;
assume K is non
empty;
then
reconsider K as non
empty
Chain of P;
consider a be
Element of P such that
A1: K
=
{a} or K
=
{(
Bottom P), a} by
Thflat01;
take a;
per cases by
A1;
suppose
B100: K
=
{a};
B101: for p st p
in K holds p
<= a by
B100,
TARSKI:def 1;
B2: for p st K
is_<=_than p holds p
>= a
proof
let p;
a
in K by
B100,
TARSKI:def 1;
hence thesis;
end;
for p st (K
is_<=_than p & for p1 st K
is_<=_than p1 holds p1
>= p) holds p
= a
proof
let p;
assume that
C1: K
is_<=_than p and
C2: for p1 st K
is_<=_than p1 holds p1
>= p;
C3: p
>= a by
B2,
C1;
a
>= p by
B101,
C2,
LATTICE3:def 9;
hence thesis by
C3,
ORDERS_2: 2;
end;
hence thesis by
B101,
B2;
end;
suppose
A2: K
=
{(
Bottom P), a};
B101: for p st p
in K holds p
<= a
proof
let p;
assume p
in K;
then p
= (
Bottom P) or p
= a by
A2,
TARSKI:def 2;
hence thesis by
YELLOW_0: 44;
end;
B2: for p st K
is_<=_than p holds p
>= a
proof
let p;
a
in K by
A2,
TARSKI:def 2;
hence thesis;
end;
for p st (K
is_<=_than p & for p1 st K
is_<=_than p1 holds p1
>= p) holds p
= a
proof
let p;
assume that
C1: K
is_<=_than p and
C2: for p1 st K
is_<=_than p1 holds p1
>= p;
C3: p
>= a by
B2,
C1;
a
>= p by
B101,
C2,
LATTICE3:def 9;
hence thesis by
C3,
ORDERS_2: 2;
end;
hence thesis by
B101,
B2;
end;
end;
theorem ::
POSET_2:7
Thflat05: for f be
Function of P, Q holds ex a be
Element of P st (K
=
{a} & (f
.: K)
=
{(f
. a)}) or (K
=
{(
Bottom P), a} & (f
.: K)
=
{(f
. (
Bottom P)), (f
. a)})
proof
let f be
Function of P, Q;
consider a be
Element of P such that
A1: K
=
{a} or K
=
{(
Bottom P), a} by
Thflat01;
take a;
set z = (
Bottom P);
A3: the
carrier of P
= (
dom f) by
FUNCT_2:def 1;
K
=
{a, a} or K
=
{(
Bottom P), a} by
A1,
ENUMSET1: 29;
then (K
=
{a, a} & (f
.: K)
=
{(f
. a), (f
. a)}) or (K
=
{(
Bottom P), a} & (f
.: K)
=
{(f
. (
Bottom P)), (f
. a)}) by
A3,
FUNCT_1: 60;
hence thesis by
ENUMSET1: 29;
end;
theorem ::
POSET_2:8
Thflat0501: for f be
Function of P, Q holds (f
. (
Bottom P))
= (
Bottom Q) implies f is
monotone
proof
let f be
Function of P, Q;
assume
A1: (f
. (
Bottom P))
= (
Bottom Q);
set z = (
Bottom P);
for p1,p2 be
Element of P st p1
<= p2 holds for q1,q2 be
Element of Q st q1
= (f
. p1) & q2
= (f
. p2) holds q1
<= q2
proof
let p1,p2 be
Element of P;
assume p1
<= p2;
then p1
= z or p1
= p2 by
Lemflat01;
hence thesis by
A1,
Lemflat01;
end;
hence thesis;
end;
theorem ::
POSET_2:9
Thflat0502: K
=
{(
Bottom P), p} implies (
sup K)
= p
proof
set z = (
Bottom P);
assume
A0: K
=
{z, p};
A1:
ex_sup_of (K,P) by
Lemflat02;
z
<= p & p
<= p by
YELLOW_0: 44;
then
A2: K
is_<=_than p by
YELLOW_0: 8,
A0;
for p1 st K
is_<=_than p1 holds p
<= p1 by
A0,
YELLOW_0: 8;
hence thesis by
YELLOW_0:def 9,
A1,
A2;
end;
registration
cluster
strict non
empty
flat
chain-complete for
Poset;
existence
proof
take the
strict non
empty
flat
Poset;
thus thesis by
Lemflat02;
end;
end
registration
cluster non
empty
flat ->
chain-complete for
Poset;
correctness by
Lemflat02;
end
theorem ::
POSET_2:10
Thflat07: for P,Q be
strict non
empty
chain-complete
flat
Poset, f be
Function of P, Q st (f
. (
Bottom P))
= (
Bottom Q) holds f is
continuous
proof
let P,Q be
strict non
empty
chain-complete
flat
Poset;
let f be
Function of P, Q;
assume
A1: (f
. (
Bottom P))
= (
Bottom Q);
then
reconsider f as
monotone
Function of P, Q by
Thflat0501;
for K be non
empty
Chain of P holds (f
. (
sup K))
<= (
sup (f
.: K))
proof
let K be non
empty
Chain of P;
reconsider M = (f
.: K) as non
empty
Chain of Q by
POSET_1: 1;
consider a be
Element of P such that
B1: (K
=
{a} & (f
.: K)
=
{(f
. a)}) or (K
=
{(
Bottom P), a} & (f
.: K)
=
{(f
. (
Bottom P)), (f
. a)}) by
Thflat05;
per cases by
A1,
B1;
suppose K
=
{a} & M
=
{(f
. a)};
then (
sup K)
= a & (
sup M)
= (f
. a) by
YELLOW_0: 39;
hence thesis;
end;
suppose K
=
{(
Bottom P), a} & M
=
{(
Bottom Q), (f
. a)};
then (
sup K)
= a & (
sup M)
= (f
. a) by
Thflat0502;
hence thesis;
end;
end;
hence thesis by
POSET_1: 8;
end;
begin
reserve X,Y for non
empty
set;
definition
let X be non
empty
set;
::
POSET_2:def2
func
FlatRelat (X) ->
Relation of (
succ X), (
succ X) equals ((
{
[X, X]}
\/
[:
{X}, X:])
\/ (
id X));
correctness
proof
set F = (
succ X);
X
in
{X} by
TARSKI:def 1;
then X
in F by
XBOOLE_0:def 3;
then
reconsider R1 =
{
[X, X]} as
Relation of F, F by
RELSET_1: 3;
A1:
{X}
c= F by
XBOOLE_1: 7;
A2: X
c= F by
XBOOLE_1: 7;
[:
{X}, X:]
c=
[:
{X}, X:];
then
reconsider R2 =
[:
{X}, X:] as
Relation of F, F by
A1,
A2,
RELSET_1: 7;
reconsider R3 = (R1
\/ R2) as
Relation of F, F;
reconsider R4 = (
id X) as
Relation of F, F by
A2,
RELSET_1: 7;
(R3
\/ R4) is
Relation of F, F;
hence thesis;
end;
end
LemFlatten01: for x,y be
Element of (
succ X) st
[x, y]
in (
FlatRelat X) holds x
= X or x
= y
proof
let x,y be
Element of (
succ X);
set a =
[x, y];
assume a
in (
FlatRelat X);
then a
in
{
[X, X]} or a
in
[:
{X}, X:] or a
in (
id X) by
LemSUM01;
then
[x, y]
=
[X, X] or x
= X or x
= y by
TARSKI:def 1,
ZFMISC_1: 105,
RELAT_1:def 10;
hence thesis by
XTUPLE_0: 1;
end;
LemFlatten02: for x,y be
Element of (
succ X) st (x
= X or x
= y) holds
[x, y]
in (
FlatRelat X)
proof
let x,y be
Element of (
succ X);
assume
A1: x
= X or x
= y;
A2: x
in
{X} or x
in X by
XBOOLE_0:def 3;
A3: y
in
{X} or y
in X by
XBOOLE_0:def 3;
set a =
[x, y];
per cases by
A1;
suppose
B1: x
= X;
per cases ;
suppose y
= X;
then a
in
{
[X, X]} by
B1,
TARSKI:def 1;
hence thesis by
LemSUM01;
end;
suppose y
<> X;
then a
in
[:
{X}, X:] by
B1,
ZFMISC_1: 105,
A3,
TARSKI:def 1;
hence thesis by
LemSUM01;
end;
end;
suppose
B2: x
= y;
per cases ;
suppose x
= X;
then a
in
{
[X, X]} by
B2,
TARSKI:def 1;
hence thesis by
LemSUM01;
end;
suppose x
<> X;
then a
in (
id X) by
B2,
RELAT_1:def 10,
A2,
TARSKI:def 1;
hence thesis by
LemSUM01;
end;
end;
end;
theorem ::
POSET_2:11
for x,y be
Element of (
succ X) holds
[x, y]
in (
FlatRelat X) iff x
= X or x
= y by
LemFlatten01,
LemFlatten02;
definition
let X be non
empty
set;
::
POSET_2:def3
func
FlatPoset (X) ->
strict non
empty
chain-complete
flat
Poset equals
RelStr (# (
succ X), (
FlatRelat X) #);
correctness
proof
reconsider IT =
RelStr (# (
succ X), (
FlatRelat X) #) as non
empty
RelStr;
X
in
{X} by
TARSKI:def 1;
then
reconsider X as
Element of IT by
XBOOLE_0:def 3;
IT is
flat
proof
take X;
thus thesis by
LemFlatten01,
LemFlatten02;
end;
hence thesis;
end;
end
theorem ::
POSET_2:12
ThFlatten04: for x,y be
Element of (
FlatPoset X) holds x
<= y iff x
= X or x
= y by
LemFlatten01,
LemFlatten02;
theorem ::
POSET_2:13
LemFlatten05: X is
Element of (
FlatPoset X)
proof
X
in
{X} by
TARSKI:def 1;
hence thesis by
XBOOLE_0:def 3;
end;
registration
let X;
reduce (
Bottom (
FlatPoset X)) to X;
reducibility
proof
set F = (
FlatPoset X);
reconsider X as
Element of F by
LemFlatten05;
for x be
Element of F holds X
<= x by
LemFlatten02;
hence thesis by
ThMin02,
LemMin01;
end;
end
definition
let x be
object;
let X,Y be non
empty
set;
let f be
Function of X, Y;
::
POSET_2:def4
func
Flatten (f,x) ->
set equals
:
DefFlatten01: (f
. x) if x
in X
otherwise Y;
correctness ;
end
definition
let X,Y be non
empty
set;
let f be
Function of X, Y;
::
POSET_2:def5
func
Flatten f ->
Function of (
FlatPoset X), (
FlatPoset Y) means
:
DefFlatten04: (it
. X)
= Y & for x be
Element of (
FlatPoset X) st x
<> X holds (it
. x)
= (f
. x);
existence
proof
set z = X;
set r = Y;
A0: not z
in X & not r
in Y;
set FX = (
FlatPoset X);
set CX = (
succ X);
z
in
{z} by
TARSKI:def 1;
then
A201: z
in CX by
XBOOLE_0:def 3;
set FY = (
FlatPoset Y);
set CY = (
succ Y);
r
in
{r} by
TARSKI:def 1;
then
A401: r
in CY by
XBOOLE_0:def 3;
deffunc
H(
object) = (
Flatten (f,$1));
A5: for x st x
in CX holds
H(x)
in CY
proof
let x;
assume x
in CX;
per cases ;
suppose
B2: x
in X;
then
C1:
H(x)
= (f
. x) by
DefFlatten01;
(f
. x)
in Y by
B2,
FUNCT_2: 5;
hence thesis by
C1,
XBOOLE_0:def 3;
end;
suppose not x
in X;
hence thesis by
DefFlatten01,
A401;
end;
end;
ex h be
Function of CX, CY st for x st x
in CX holds (h
. x)
=
H(x) from
FUNCT_2:sch 2(
A5);
then
consider IT be
Function of CX, CY such that
A6: for x st x
in CX holds (IT
. x)
=
H(x);
reconsider IT as
Function of FX, FY;
A7: (IT
. z)
=
H(z) by
A201,
A6
.= r by
A0,
DefFlatten01;
for x be
Element of FX st x
<> z holds (IT
. x)
= (f
. x)
proof
let x be
Element of FX;
assume
B1: x
<> z;
B3: x
in
{z} or x
in X by
XBOOLE_0:def 3;
(IT
. x)
=
H(x) by
A6
.= (f
. x) by
DefFlatten01,
B1,
B3,
TARSKI:def 1;
hence thesis;
end;
hence thesis by
A7;
end;
uniqueness
proof
set FX = (
FlatPoset X);
set FY = (
FlatPoset Y);
set CX = (
succ X);
set CY = (
succ Y);
let IT1,IT2 be
Function of FX, FY;
assume
B1: ((IT1
. X)
= Y & for x be
Element of FX st x
<> X holds (IT1
. x)
= (f
. x)) & ((IT2
. X)
= Y & for x be
Element of FX st x
<> X holds (IT2
. x)
= (f
. x));
reconsider IT1, IT2 as
Function of CX, CY;
for x be
Element of CX holds (IT1
. x)
= (IT2
. x)
proof
let x be
Element of CX;
per cases ;
suppose x
= X;
hence thesis by
B1;
end;
suppose
C1: x
<> X;
then (IT1
. x)
= (f
. x) by
B1
.= (IT2
. x) by
C1,
B1;
hence thesis;
end;
end;
hence thesis;
end;
end
registration
let X,Y be non
empty
set;
let f be
Function of X, Y;
cluster (
Flatten f) ->
continuous;
coherence
proof
((
Flatten f)
. (
Bottom (
FlatPoset X)))
= (
Bottom (
FlatPoset Y)) by
DefFlatten04;
hence thesis by
Thflat07;
end;
end
theorem ::
POSET_2:14
for f be
Function of X, Y st x
in X holds ((
Flatten f)
. x)
in Y
proof
let f be
Function of X, Y;
assume
A1: x
in X;
then
reconsider xx = x as
set;
A2: not xx
in xx;
set FX = (
FlatPoset X);
reconsider x as
Element of FX by
A1,
XBOOLE_0:def 3;
(f
. x)
in Y by
A1,
FUNCT_2: 5;
hence thesis by
DefFlatten04,
A1,
A2;
end;
definition
let X, Y;
::
POSET_2:def6
func
FlatConF (X,Y) ->
strict
chain-complete non
empty
Poset equals (
ConPoset ((
FlatPoset X),(
FlatPoset Y)));
coherence ;
end
registration
let L be
flat
Poset;
cluster ->
finite for
Chain of L;
coherence
proof
let A be
Chain of L;
per cases ;
suppose
A1: A is non
empty;
then
reconsider LL = L as non
empty
Poset;
reconsider AA = A as non
empty
Chain of LL by
A1;
ex a be
Element of LL st AA
=
{a} or AA
=
{(
Bottom LL), a} by
Thflat01;
hence thesis;
end;
suppose A is
empty;
hence thesis;
end;
end;
end
registration
cluster non
empty
flat
lower-bounded for
LATTICE;
existence
proof
set A =
{
{} };
reconsider R = (
id A) as
Relation of A;
reconsider R as
Order of A;
take IT =
RelStr (# A, R #);
reconsider z =
{} as
Element of IT by
TARSKI:def 1;
ex a be
Element of IT st a
is_<=_than the
carrier of IT & (for x,y be
Element of IT holds (x
<= y iff x
= a or x
= y))
proof
b1: for x be
Element of IT holds z
<= x by
TARSKI:def 1;
for x,y be
Element of IT holds (x
<= y iff x
= z or x
= y) by
TARSKI:def 1;
hence thesis by
b1,
LemMin01;
end;
hence thesis;
end;
end
theorem ::
POSET_2:15
CardA1: for L be non
empty
LATTICE, x be
Element of L, A be
Chain of x, x holds (
card A)
= 1
proof
let L be non
empty
LATTICE, x be
Element of L, A be
Chain of x, x;
for z be
Element of L st z
in A holds z
in
{x}
proof
let z be
Element of L;
assume z
in A;
then x
<= z & z
<= x by
LATTICE7:def 2;
then z
= x by
ORDERS_2: 2;
hence thesis by
TARSKI:def 1;
end;
then A
c=
{x} by
LATTICE7:def 1;
hence thesis by
CARD_2: 42,
ZFMISC_1: 33;
end;
theorem ::
POSET_2:16
for L be non
empty
flat
lower-bounded
LATTICE, x be
Element of L, A be
Chain of (
Bottom L), x holds (
card A)
<= 2
proof
let L be non
empty
flat
lower-bounded
LATTICE, x be
Element of L, A be
Chain of (
Bottom L), x;
S0: (
Bottom L)
<= x by
YELLOW_0: 44;
per cases ;
suppose
KK: (
Bottom L)
<> x;
consider b be
Element of L such that
H1: A
=
{b} or A
=
{(
Bottom L), b} by
Thflat01;
H2: x
in A & (
Bottom L)
in A by
LATTICE7:def 2,
S0;
A
<>
{b}
proof
assume A
=
{b};
then x
= b & b
= (
Bottom L) by
TARSKI:def 1,
H2;
hence thesis by
KK;
end;
hence (
card A)
<= 2 by
CARD_2: 50,
H1;
end;
suppose (
Bottom L)
= x;
then (
card A)
= 1 by
CardA1;
hence thesis;
end;
end;
theorem ::
POSET_2:17
for L be
finite
lower-bounded
antisymmetric non
empty
LATTICE holds L is
flat iff for x be
Element of L holds (
height x)
<= 2
proof
let L be
finite
lower-bounded
antisymmetric non
empty
LATTICE;
hereby
assume
A0: L is
flat;
let x be
Element of L;
S0: (
Bottom L)
<= x by
YELLOW_0: 44;
reconsider D =
{(
Bottom L), x} as
Chain of (
Bottom L), x by
LATTICE7: 1,
YELLOW_0: 44;
per cases ;
suppose
KK: (
Bottom L)
<> x;
then
t1: (
card D)
= 2 by
CARD_2: 57;
for A be
Chain of (
Bottom L), x holds (
card A)
<= 2
proof
let A be
Chain of (
Bottom L), x;
consider b be
Element of L such that
H1: A
=
{b} or A
=
{(
Bottom L), b} by
Thflat01,
A0;
H2: x
in A & (
Bottom L)
in A by
LATTICE7:def 2,
S0;
A
<>
{b}
proof
assume A
=
{b};
then x
= b & b
= (
Bottom L) by
TARSKI:def 1,
H2;
hence thesis by
KK;
end;
hence (
card A)
<= 2 by
CARD_2: 50,
H1;
end;
hence (
height x)
<= 2 by
LATTICE7:def 3,
t1;
end;
suppose (
Bottom L)
= x;
then (
height x)
= 1 by
LATTICE7: 6;
hence (
height x)
<= 2;
end;
end;
assume
AA: for x be
Element of L holds (
height x)
<= 2;
ex a be
Element of L st for x,y be
Element of L holds x
<= y iff x
= a or x
= y
proof
take a = (
Bottom L);
let x,y be
Element of L;
hereby
assume
AS: x
<= y;
per cases ;
suppose x
= a & y
= x;
hence x
= a or x
= y;
end;
suppose x
<> a & y
= x;
hence x
= a or x
= y;
end;
suppose
a1: x
<> a & y
<> x;
then a
< x by
YELLOW_0: 44;
then (
height a)
< (
height x) by
LATTICE7: 2;
then 1
< (
height x) by
LATTICE7: 6;
then
y1: (1
+ 1)
<= (
height x) by
NAT_1: 13;
x
< y by
a1,
AS;
then
Y2: (
height x)
< (
height y) by
LATTICE7: 2;
(
height x)
<= 2 by
AA;
then (
height x)
= 2 by
y1,
XXREAL_0: 1;
hence x
= a or x
= y by
AA,
Y2;
end;
suppose x
= a & y
<> x;
hence x
= a or x
= y;
end;
end;
thus thesis by
YELLOW_0: 44;
end;
hence thesis;
end;
begin
reserve D for
Subset of X;
reserve I for
Function of X, Y;
reserve J for
Function of
[:X, Y:], Y;
reserve E for
Function of X, X;
definition
let X be non
empty
set;
let D be
Subset of X;
let E be
Function of X, X;
::
POSET_2:def7
pred E
is_well_founded_with_minimal_set D means ex l be
Function of X,
NAT st for x be
Element of X holds ((l
. x)
<=
0 implies x
in D) & ( not x
in D implies (l
. (E
. x))
< (l
. x));
end
definition
let X,Y be non
empty
set;
let D be
Subset of X;
let I be
Function of X, Y;
let J be
Function of
[:X, Y:], Y;
let x,y be
object;
::
POSET_2:def8
func
BaseFunc01 (x,y,I,J,D) ->
set equals
:
DefBaseFunc01: (I
. x) if x
in D,
(J
.
[x, y]) if ( not x
in D) & x
in X & y
in Y
otherwise Y;
correctness ;
end
definition
let X,Y be non
empty
set;
let D be
Subset of X;
let I be
Function of X, Y;
let J be
Function of
[:X, Y:], Y;
let E be
Function of X, X;
let h be
object;
assume
A00: h is
continuous
Function of (
FlatPoset X), (
FlatPoset Y);
::
POSET_2:def9
func
RecFunc01 (h,E,I,J,D) ->
continuous
Function of (
FlatPoset X), (
FlatPoset Y) means
:
DefRecFunc01: for x be
Element of (
FlatPoset X), f be
continuous
Function of (
FlatPoset X), (
FlatPoset Y) st h
= f holds (it
. x)
= (
BaseFunc01 (x,(f
. ((
Flatten E)
. x)),I,J,D));
existence
proof
set z = X;
set r = Y;
A0: not z
in X & not r
in Y;
set FX = (
FlatPoset X);
set CX = (
succ X);
z
in
{z} by
TARSKI:def 1;
then
reconsider z as
Element of FX by
XBOOLE_0:def 3;
set FY = (
FlatPoset Y);
set CY = (
succ Y);
r
in
{r} by
TARSKI:def 1;
then
A401: r
in CY by
XBOOLE_0:def 3;
reconsider h as
continuous
Function of FX, FY by
A00;
defpred
U[
object,
object] means for x be
set, f be
continuous
Function of FX, FY st x is
Element of (
FlatPoset X) & h
= f & x
= $1 holds $2
= (
BaseFunc01 (x,(f
. ((
Flatten E)
. x)),I,J,D));
deffunc
H(
object) = (
BaseFunc01 ($1,(h
. ((
Flatten E)
. $1)),I,J,D));
A5: for x0 be
object st x0
in CX holds ex y be
object st y
in CY &
U[x0, y]
proof
let x0 be
object;
assume x0
in CX;
set x1 = (h
. ((
Flatten E)
. x0));
set y =
H(x0);
B200:
U[x0, y];
per cases ;
suppose
B2: x0
in X;
y
in CY
proof
per cases ;
suppose
B3: x1
in Y;
then
C0:
[x0, x1]
in
[:X, Y:] by
B2,
ZFMISC_1:def 2;
per cases ;
suppose x0
in D;
then
C01:
H(x0)
= (I
. x0) by
DefBaseFunc01;
(I
. x0)
in Y by
B2,
FUNCT_2: 5;
hence thesis by
C01,
XBOOLE_0:def 3;
end;
suppose not x0
in D;
then
C01:
H(x0)
= (J
.
[x0, x1]) by
DefBaseFunc01,
B2,
B3;
(J
.
[x0, x1])
in Y by
C0,
FUNCT_2: 5;
hence thesis by
C01,
XBOOLE_0:def 3;
end;
end;
suppose
B3: not x1
in Y;
per cases ;
suppose x0
in D;
then
C01:
H(x0)
= (I
. x0) by
DefBaseFunc01;
(I
. x0)
in Y by
B2,
FUNCT_2: 5;
hence thesis by
C01,
XBOOLE_0:def 3;
end;
suppose not x0
in D;
hence thesis by
B3,
A401,
DefBaseFunc01;
end;
end;
end;
hence thesis by
B200;
end;
suppose not x0
in X;
then not (x0
in D or (x0
in X & x1
in Y));
then
H(x0)
= r by
DefBaseFunc01;
hence thesis by
A401,
B200;
end;
end;
consider IT be
Function of CX, CY such that
A6: for x st x
in CX holds
U[x, (IT
. x)] from
FUNCT_2:sch 1(
A5);
reconsider IT as
Function of FX, FY;
A601: not z
in D by
A0;
A7: (IT
. z)
= (
BaseFunc01 (z,(h
. ((
Flatten E)
. z)),I,J,D)) by
A6
.= r by
A0,
DefBaseFunc01,
A601;
(IT
. (
Bottom FX))
= (
Bottom FY) by
A7;
then
reconsider IT as
continuous
Function of FX, FY by
Thflat07;
take IT;
thus thesis by
A6;
end;
uniqueness
proof
set FX = (
FlatPoset X);
set CX = (
succ X);
set FY = (
FlatPoset Y);
set CY = (
succ Y);
reconsider h as
continuous
Function of FX, FY by
A00;
for g1,g2 be
continuous
Function of FX, FY st ((for x be
Element of FX, f be
continuous
Function of FX, FY st h
= f holds (g1
. x)
= (
BaseFunc01 (x,(f
. ((
Flatten E)
. x)),I,J,D))) & (for x be
Element of FX, f be
continuous
Function of FX, FY st h
= f holds (g2
. x)
= (
BaseFunc01 (x,(f
. ((
Flatten E)
. x)),I,J,D)))) holds g1
= g2
proof
let g1,g2 be
continuous
Function of FX, FY;
assume
B1: (for x be
Element of FX, f be
continuous
Function of FX, FY st h
= f holds (g1
. x)
= (
BaseFunc01 (x,(f
. ((
Flatten E)
. x)),I,J,D))) & (for x be
Element of FX, f be
continuous
Function of FX, FY st h
= f holds (g2
. x)
= (
BaseFunc01 (x,(f
. ((
Flatten E)
. x)),I,J,D)));
for x be
Element of FX holds (g1
. x)
= (g2
. x)
proof
let x be
Element of FX;
(g1
. x)
= (
BaseFunc01 (x,(h
. ((
Flatten E)
. x)),I,J,D)) by
B1
.= (g2
. x) by
B1;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
end
theorem ::
POSET_2:18
Threcursive01: ex W be
continuous
Function of (
FlatConF (X,Y)), (
FlatConF (X,Y)) st for f be
Element of (
ConFuncs ((
FlatPoset X),(
FlatPoset Y))) holds (W
. f)
= (
RecFunc01 (f,E,I,J,D))
proof
set z = X;
set r = Y;
set FX = (
FlatPoset X);
set CX = (
succ X);
set FY = (
FlatPoset Y);
set CY = (
succ Y);
set FlatC = (
FlatConF (X,Y));
set CFXY = (
ConFuncs (FX,FY));
set CRFXY = (
ConRelat (FX,FY));
deffunc
H(
object) = (
RecFunc01 ($1,E,I,J,D));
A7: for h be
continuous
Function of FX, FY holds h
in CFXY
proof
let h be
continuous
Function of FX, FY;
h
in (
Funcs (the
carrier of FX,the
carrier of FY)) by
FUNCT_2: 8;
hence thesis;
end;
A8: for h be
set st h
in CFXY holds h is
continuous
Function of FX, FY
proof
let h be
set;
assume h
in CFXY;
then
consider x be
Element of (
Funcs (the
carrier of FX,the
carrier of FY)) such that
B1: h
= x & ex g be
continuous
Function of FX, FY st g
= x;
thus thesis by
B1;
end;
A9: for f be
object st f
in CFXY holds
H(f)
in CFXY by
A7;
ex W be
Function of CFXY, CFXY st for f be
object st f
in CFXY holds (W
. f)
=
H(f) from
FUNCT_2:sch 2(
A9);
then
consider IT be
Function of CFXY, CFXY such that
A10: for f be
object st f
in CFXY holds (IT
. f)
=
H(f);
IT is
continuous
Function of FlatC, FlatC
proof
B2: for f be
continuous
Function of FX, FY holds ex g be
continuous
Function of FX, FY st g
= (IT
. f)
proof
let f be
continuous
Function of FX, FY;
set g = (IT
. f);
f
in CFXY by
A7;
then
reconsider g as
continuous
Function of FX, FY by
A8,
FUNCT_2: 5;
take g;
thus thesis;
end;
B3: for f,g be
continuous
Function of FX, FY st g
= (IT
. f) holds for x be
Element of FX holds (g
. x)
= (
BaseFunc01 (x,(f
. ((
Flatten E)
. x)),I,J,D))
proof
let f,g be
continuous
Function of FX, FY;
assume
C1: g
= (IT
. f);
for x be
Element of FX holds (g
. x)
= (
BaseFunc01 (x,(f
. ((
Flatten E)
. x)),I,J,D))
proof
let x be
Element of FX;
(g
. x)
= ((
RecFunc01 (f,E,I,J,D))
. x) by
A7,
A10,
C1
.= (
BaseFunc01 (x,(f
. ((
Flatten E)
. x)),I,J,D)) by
DefRecFunc01;
hence thesis;
end;
hence thesis;
end;
reconsider IT as
Function of FlatC, FlatC;
IT is
monotone
proof
for f1,f2 be
Element of FlatC st f1
<= f2 holds for g1,g2 be
Element of FlatC st g1
= (IT
. f1) & g2
= (IT
. f2) holds g1
<= g2
proof
let f1,f2 be
Element of FlatC such that
C1: f1
<= f2;
let g1,g2 be
Element of FlatC such that
C2: g1
= (IT
. f1) & g2
= (IT
. f2);
consider f10,f20 be
Function of FX, FY such that
C401: f1
= f10 & f2
= f20 & f10
<= f20 by
POSET_1:def 7,
C1;
reconsider f10, f20 as
continuous
Function of FX, FY by
C401,
A8;
reconsider g10 = g1 as
continuous
Function of FX, FY by
A8;
reconsider g20 = g2 as
continuous
Function of FX, FY by
A8;
for x be
Element of FX holds (g10
. x)
<= (g20
. x)
proof
let x be
Element of FX;
reconsider y = ((
Flatten E)
. x) as
Element of FX;
set y1 = (f10
. y);
set y2 = (f20
. y);
D1: (g10
. x)
= (
BaseFunc01 (x,y1,I,J,D)) by
B3,
C2,
C401;
D2: (g20
. x)
= (
BaseFunc01 (x,y2,I,J,D)) by
B3,
C2,
C401;
per cases by
ThFlatten04,
C401,
YELLOW_2: 9;
suppose y1
= r;
then
D000: not y1
in Y;
per cases ;
suppose
D001: x
in D;
then (g10
. x)
= (I
. x) by
D1,
DefBaseFunc01;
hence thesis by
D2,
D001,
DefBaseFunc01;
end;
suppose not x
in D;
then (g10
. x)
= r by
D000,
D1,
DefBaseFunc01;
hence thesis by
LemFlatten02;
end;
end;
suppose y1
= y2;
hence thesis by
D1,
B3,
C2,
C401;
end;
end;
then g10
<= g20 by
YELLOW_2: 9;
hence thesis by
POSET_1:def 7;
end;
hence thesis;
end;
then
reconsider IT as
monotone
Function of FlatC, FlatC;
for F be non
empty
Chain of FlatC holds (IT
. (
sup F))
<= (
sup (IT
.: F))
proof
let F be non
empty
Chain of FlatC;
reconsider G = (IT
.: F) as non
empty
Chain of FlatC by
POSET_1: 1;
(IT
. (
sup F))
<= (
sup G)
proof
reconsider F, G as non
empty
Chain of (
ConPoset (FX,FY));
set sf = (
sup F);
D1: sf
= (
sup_func F) by
POSET_1: 11;
then
reconsider sf as
continuous
Function of FX, FY;
set sg = (
sup G);
D3: sg
= (
sup_func G) by
POSET_1: 11;
then
reconsider sg as
continuous
Function of FX, FY;
consider g be
continuous
Function of FX, FY such that
D5: g
= (IT
. sf) by
B2;
for x be
Element of FX holds (g
. x)
<= (sg
. x)
proof
let x be
Element of FX;
reconsider x1 = ((
Flatten E)
. x) as
Element of FX;
reconsider M = (F
-image x1) as non
empty
Chain of FY;
consider a be
Element of FY such that
D000: M
=
{a} or M
=
{(
Bottom FY), a} by
Thflat01;
D001: (
sup M)
= a by
D000,
YELLOW_0: 39,
Thflat0502;
D002: (g
. x)
= (
BaseFunc01 (x,(sf
. x1),I,J,D)) by
B3,
D5
.= (
BaseFunc01 (x,a,I,J,D)) by
D001,
POSET_1:def 10,
D1;
a
in (F
-image x1) by
TARSKI:def 1,
TARSKI:def 2,
D000;
then
consider q1 be
Element of FY such that
D003: q1
= a & ex f1 be
continuous
Function of FX, FY st f1
in F & q1
= (f1
. x1);
consider f1 be
continuous
Function of FX, FY such that
D004: f1
in F & a
= (f1
. x1) by
D003;
reconsider f01 = f1 as
Element of FlatC by
A7;
reconsider g01 = (IT
. f01) as
continuous
Function of FX, FY by
A8;
D005: (g01
. x)
= (g
. x) by
B3,
D004,
D002;
reconsider N = (G
-image x) as non
empty
Chain of FY;
D006: (sg
. x)
= (
sup N) by
POSET_1:def 10,
D3;
(
dom IT)
= CFXY by
FUNCT_2:def 1;
then
[f01, g01]
in IT by
FUNCT_1:def 2;
then g01
in (IT
.: F) by
RELAT_1:def 13,
D004;
then (g01
. x)
in N;
hence thesis by
D005,
Thsup01,
D006;
end;
then g
<= sg by
YELLOW_2: 9;
hence thesis by
D5,
POSET_1:def 7;
end;
hence thesis;
end;
hence thesis by
POSET_1: 8;
end;
then
reconsider IT as
continuous
Function of FlatC, FlatC;
for f be
Element of CFXY holds (IT
. f)
= (
RecFunc01 (f,E,I,J,D)) by
A10;
hence thesis;
end;
theorem ::
POSET_2:19
Threcursive02: ex f be
set st f
in (
ConFuncs ((
FlatPoset X),(
FlatPoset Y))) & f
= (
RecFunc01 (f,E,I,J,D))
proof
set FX = (
FlatPoset X);
set FY = (
FlatPoset Y);
set FlatC = (
FlatConF (X,Y));
set CFXY = (
ConFuncs (FX,FY));
set CRFXY = (
ConRelat (FX,FY));
consider W be
continuous
Function of FlatC, FlatC such that
A4: for f be
Element of CFXY holds (W
. f)
= (
RecFunc01 (f,E,I,J,D)) by
Threcursive01;
reconsider W as
monotone
Function of FlatC, FlatC;
reconsider f = (
least_fix_point W) as
Element of FlatC;
A5: f
is_a_fixpoint_of W by
POSET_1:def 5;
A6: f
= (W
. f) by
A5,
ABIAN:def 3;
take f;
thus thesis by
A4,
A6;
end;
theorem ::
POSET_2:20
Threcursive03: E
is_well_founded_with_minimal_set D implies ex f be
continuous
Function of (
FlatPoset X), (
FlatPoset Y) st for x be
Element of X holds (f
. x)
in Y & (f
. x)
= (
BaseFunc01 (x,(f
. (E
. x)),I,J,D))
proof
set z = X;
set r = Y;
assume
A0: E
is_well_founded_with_minimal_set D;
A1: not z
in X & not r
in Y;
set FX = (
FlatPoset X);
set CX = (
succ X);
set FY = (
FlatPoset Y);
set CY = (
succ Y);
consider f be
set such that
A5: f
in (
ConFuncs ((
FlatPoset X),(
FlatPoset Y))) & f
= (
RecFunc01 (f,E,I,J,D)) by
Threcursive02;
reconsider f as
continuous
Function of (
FlatPoset X), (
FlatPoset Y) by
A5;
consider l be
Function of X,
NAT such that
A6: for x0 be
Element of X holds ((l
. x0)
<=
0 implies x0
in D) & ( not x0
in D implies (l
. (E
. x0))
< (l
. x0)) by
A0;
defpred
P[
Nat] means for x0 be
Element of X st (l
. x0)
<= $1 holds ((f
. x0)
in Y & (f
. x0)
= (
BaseFunc01 (x0,(f
. (E
. x0)),I,J,D)));
A7:
P[
0 ]
proof
let x0 be
Element of X;
assume
b1: (l
. x0)
<=
0 ;
B2: x0
in X;
reconsider x0 as
Element of FX by
XBOOLE_0:def 3;
B3: x0
<> z by
B2;
B5: (f
. x0)
= (
BaseFunc01 (x0,(f
. ((
Flatten E)
. x0)),I,J,D)) by
DefRecFunc01,
A5
.= (
BaseFunc01 (x0,(f
. (E
. x0)),I,J,D)) by
B3,
DefFlatten04;
then (f
. x0)
= (I
. x0) by
DefBaseFunc01,
b1,
A6;
hence thesis by
B5,
FUNCT_2: 5;
end;
A8: for k st
P[k] holds
P[(k
+ 1)]
proof
let k;
assume
B0:
P[k];
let x0 be
Element of X;
assume
B1: (l
. x0)
<= (k
+ 1);
reconsider x0 as
Element of FX by
XBOOLE_0:def 3;
B3: x0
<> z by
A1;
reconsider x1 = (E
. x0) as
Element of X by
FUNCT_2: 5;
B5: (f
. x0)
= (
BaseFunc01 (x0,(f
. ((
Flatten E)
. x0)),I,J,D)) by
DefRecFunc01,
A5
.= (
BaseFunc01 (x0,(f
. x1),I,J,D)) by
B3,
DefFlatten04;
per cases ;
suppose x0
in D;
then (f
. x0)
= (I
. x0) by
DefBaseFunc01,
B5;
hence thesis by
FUNCT_2: 5,
B5;
end;
suppose
C0: not x0
in D;
reconsider x0 as
Element of X;
((l
. x1)
+ 1)
<= (l
. x0) by
NAT_1: 13,
A6,
C0;
then ((l
. x1)
+ 1)
<= (k
+ 1) by
B1,
XXREAL_0: 2;
then (l
. x1)
<= k by
XREAL_1: 8;
then
C1: (f
. x1)
in Y by
B0;
C4:
[x0, (f
. x1)]
in
[:X, Y:] by
C1,
ZFMISC_1:def 2;
(J
.
[x0, (f
. x1)])
in Y by
C4,
FUNCT_2: 5;
hence thesis by
B5,
DefBaseFunc01,
C0,
C1;
end;
end;
A9: for k be
Nat holds
P[k] from
NAT_1:sch 2(
A7,
A8);
for x be
Element of X holds (f
. x)
in Y & (f
. x)
= (
BaseFunc01 (x,(f
. (E
. x)),I,J,D))
proof
let x be
Element of X;
reconsider k = (l
. x) as
Nat;
(l
. x)
<= k;
hence thesis by
A9;
end;
hence thesis;
end;
Lemrecursive04: E
is_well_founded_with_minimal_set D implies ex f be
Function of X, Y st for x be
Element of X holds (f
. x)
= (
BaseFunc01 (x,(f
. (E
. x)),I,J,D))
proof
assume
A1: E
is_well_founded_with_minimal_set D;
set FX = (
FlatPoset X);
set CX = (
succ X);
A02: X
c= CX by
XBOOLE_1: 7;
set FY = (
FlatPoset Y);
set CY = (
succ Y);
consider f1 be
continuous
Function of FX, FY such that
A3: for x be
Element of X holds ((f1
. x)
in Y & (f1
. x)
= (
BaseFunc01 (x,(f1
. (E
. x)),I,J,D))) by
A1,
Threcursive03;
reconsider f1 as
Function of CX, CY;
reconsider f = (f1
| X) as
Function of X, CY by
A02,
FUNCT_2: 32;
for x be
Element of X holds (f
. x)
in Y
proof
let x be
Element of X;
(f1
. x)
in Y by
A3;
hence thesis by
FUNCT_1: 49;
end;
then (
rng f)
c= Y by
FUNCT_2: 114;
then
reconsider f as
Function of X, Y by
FUNCT_2: 6;
for x be
Element of X holds (f
. x)
= (
BaseFunc01 (x,(f
. (E
. x)),I,J,D))
proof
let x be
Element of X;
reconsider x1 = (E
. x) as
Element of X;
(f
. x)
= (f1
. x) by
FUNCT_1: 49
.= (
BaseFunc01 (x,(f1
. x1),I,J,D)) by
A3;
hence thesis by
FUNCT_1: 49;
end;
hence thesis;
end;
theorem ::
POSET_2:21
E
is_well_founded_with_minimal_set D implies ex f be
Function of X, Y st for x be
Element of X holds (x
in D implies (f
. x)
= (I
. x)) & ( not x
in D implies (f
. x)
= (J
.
[x, (f
. (E
. x))]))
proof
assume E
is_well_founded_with_minimal_set D;
then
consider f be
Function of X, Y such that
A1: for x be
Element of X holds (f
. x)
= (
BaseFunc01 (x,(f
. (E
. x)),I,J,D)) by
Lemrecursive04;
take f;
let x be
Element of X;
(f
. x)
= (
BaseFunc01 (x,(f
. (E
. x)),I,J,D)) by
A1;
hence thesis by
DefBaseFunc01;
end;
theorem ::
POSET_2:22
for f1,f2 be
Function of X, Y holds E
is_well_founded_with_minimal_set D & (for x be
Element of X holds (x
in D implies (f1
. x)
= (I
. x)) & ( not x
in D implies (f1
. x)
= (J
.
[x, (f1
. (E
. x))]))) & (for x be
Element of X holds (x
in D implies (f2
. x)
= (I
. x)) & ( not x
in D implies (f2
. x)
= (J
.
[x, (f2
. (E
. x))]))) implies f1
= f2
proof
let f1,f2 be
Function of X, Y;
assume
A0: E
is_well_founded_with_minimal_set D & (for x be
Element of X holds (x
in D implies (f1
. x)
= (I
. x)) & ( not x
in D implies (f1
. x)
= (J
.
[x, (f1
. (E
. x))]))) & (for x be
Element of X holds (x
in D implies (f2
. x)
= (I
. x)) & ( not x
in D implies (f2
. x)
= (J
.
[x, (f2
. (E
. x))])));
then
consider l be
Function of X,
NAT such that
A1: for x be
Element of X holds ((l
. x)
<=
0 implies x
in D) & ( not x
in D implies (l
. (E
. x))
< (l
. x));
defpred
P[
Nat] means for x be
Element of X st (l
. x)
<= $1 holds (f1
. x)
= (f2
. x);
A2:
P[
0 ]
proof
let x be
Element of X;
assume
b1: (l
. x)
<=
0 ;
then (f1
. x)
= (I
. x) by
A0,
A1
.= (f2
. x) by
A0,
b1,
A1;
hence thesis;
end;
A3: for k st
P[k] holds
P[(k
+ 1)]
proof
let k;
assume
B0:
P[k];
let x be
Element of X;
assume
B1: (l
. x)
<= (k
+ 1);
per cases ;
suppose
C0: x
in D;
(f1
. x)
= (I
. x) by
A0,
C0
.= (f2
. x) by
A0,
C0;
hence thesis;
end;
suppose
C0: not x
in D;
reconsider x1 = (E
. x) as
Element of X;
reconsider x as
Element of X;
((l
. x1)
+ 1)
<= (l
. x) by
NAT_1: 13,
A1,
C0;
then
c2: ((l
. x1)
+ 1)
<= (k
+ 1) by
B1,
XXREAL_0: 2;
(f1
. x)
= (J
.
[x, (f1
. x1)]) by
A0,
C0
.= (J
.
[x, (f2
. x1)]) by
c2,
B0,
XREAL_1: 8
.= (f2
. x) by
A0,
C0;
hence thesis;
end;
end;
A4: for k be
Nat holds
P[k] from
NAT_1:sch 2(
A2,
A3);
for x be
Element of X holds (f1
. x)
= (f2
. x)
proof
let x be
Element of X;
reconsider k = (l
. x) as
Nat;
(l
. x)
<= k;
hence thesis by
A4;
end;
hence thesis;
end;
begin
reserve D for
Subset of X;
reserve I,I1,I2 for
Function of X, Y;
reserve J,J1,J2 for
Function of
[:X, Y, Y:], Y;
reserve E1,E2 for
Function of X, X;
definition
let X be non
empty
set;
let D be
Subset of X;
let E1,E2 be
Function of X, X;
::
POSET_2:def10
pred E1,E2
is_well_founded_with_minimal_set D means ex l be
Function of X,
NAT st for x be
Element of X holds ((l
. x)
<=
0 implies x
in D) & ( not x
in D implies (l
. (E1
. x))
< (l
. x) & (l
. (E2
. x))
< (l
. x));
end
definition
let X,Y be non
empty
set;
let D be
Subset of X;
let I be
Function of X, Y;
let J be
Function of
[:X, Y, Y:], Y;
let x,y1,y2 be
object;
::
POSET_2:def11
func
BaseFunc02 (x,y1,y2,I,J,D) ->
set equals
:
DefBaseFunc02: (I
. x) if x
in D,
(J
.
[x, y1, y2]) if ( not x
in D) & (x
in X & y1
in Y & y2
in Y)
otherwise Y;
correctness ;
end
definition
let X,Y be non
empty
set;
let D be
Subset of X;
let I be
Function of X, Y;
let J be
Function of
[:X, Y, Y:], Y;
let E1,E2 be
Function of X, X;
let h1,h2 be
object;
assume
A00: h1 is
continuous
Function of (
FlatPoset X), (
FlatPoset Y) & h2 is
continuous
Function of (
FlatPoset X), (
FlatPoset Y);
::
POSET_2:def12
func
RecFunc02 (h1,h2,E1,E2,I,J,D) ->
continuous
Function of (
FlatPoset X), (
FlatPoset Y) means
:
DefRecFunc02: for x be
Element of (
FlatPoset X), f1,f2 be
continuous
Function of (
FlatPoset X), (
FlatPoset Y) st h1
= f1 & h2
= f2 holds (it
. x)
= (
BaseFunc02 (x,(f1
. ((
Flatten E1)
. x)),(f2
. ((
Flatten E2)
. x)),I,J,D));
existence
proof
set z = X;
set r = Y;
A0: not X
in X & not Y
in Y;
set FX = (
FlatPoset X);
set CX = (
succ X);
z
in
{z} by
TARSKI:def 1;
then
reconsider z as
Element of FX by
XBOOLE_0:def 3;
set FY = (
FlatPoset Y);
set CY = (
succ Y);
Y
in
{Y} by
TARSKI:def 1;
then
A401: Y
in CY by
XBOOLE_0:def 3;
reconsider h1, h2 as
continuous
Function of FX, FY by
A00;
defpred
U[
object,
object] means for x be
set, f1,f2 be
continuous
Function of FX, FY st x is
Element of (
FlatPoset X) & h1
= f1 & h2
= f2 & x
= $1 holds $2
= (
BaseFunc02 (x,(f1
. ((
Flatten E1)
. x)),(f2
. ((
Flatten E2)
. x)),I,J,D));
deffunc
H(
object) = (
BaseFunc02 ($1,(h1
. ((
Flatten E1)
. $1)),(h2
. ((
Flatten E2)
. $1)),I,J,D));
A5: for x0 be
object st x0
in CX holds ex y st y
in CY &
U[x0, y]
proof
let x0 be
object;
assume x0
in CX;
set x1 = (h1
. ((
Flatten E1)
. x0));
set x2 = (h2
. ((
Flatten E2)
. x0));
set y =
H(x0);
B200:
U[x0, y];
per cases ;
suppose
B2: x0
in X;
y
in CY
proof
per cases ;
suppose
B3: x1
in Y & x2
in Y;
then
C0:
[x0, x1, x2]
in
[:X, Y, Y:] by
B2,
MCART_1: 69;
per cases ;
suppose x0
in D;
then
C01:
H(x0)
= (I
. x0) by
DefBaseFunc02;
(I
. x0)
in Y by
B2,
FUNCT_2: 5;
hence thesis by
C01,
XBOOLE_0:def 3;
end;
suppose not x0
in D;
then
C01:
H(x0)
= (J
.
[x0, x1, x2]) by
DefBaseFunc02,
B2,
B3;
(J
.
[x0, x1, x2])
in Y by
C0,
FUNCT_2: 5;
hence thesis by
C01,
XBOOLE_0:def 3;
end;
end;
suppose
B3: not (x1
in Y & x2
in Y);
per cases ;
suppose x0
in D;
then
C01:
H(x0)
= (I
. x0) by
DefBaseFunc02;
(I
. x0)
in Y by
B2,
FUNCT_2: 5;
hence thesis by
C01,
XBOOLE_0:def 3;
end;
suppose not x0
in D;
hence thesis by
A401,
DefBaseFunc02,
B3;
end;
end;
end;
hence thesis by
B200;
end;
suppose not x0
in X;
then not ((x0
in D) or (x0
in X & x1
in Y & x2
in Y));
then
H(x0)
= Y by
DefBaseFunc02;
hence thesis by
A401,
B200;
end;
end;
consider IT be
Function of CX, CY such that
A6: for x be
object st x
in CX holds
U[x, (IT
. x)] from
FUNCT_2:sch 1(
A5);
reconsider IT as
Function of FX, FY;
A7: not z
in D by
A0;
A8: (IT
. z)
= (
BaseFunc02 (z,(h1
. ((
Flatten E1)
. z)),(h2
. ((
Flatten E2)
. z)),I,J,D)) by
A6
.= r by
A0,
DefBaseFunc02,
A7;
(IT
. (
Bottom FX))
= (
Bottom FY) by
A8;
then
reconsider IT as
continuous
Function of FX, FY by
Thflat07;
take IT;
thus thesis by
A6;
end;
uniqueness
proof
set FX = (
FlatPoset X);
set CX = (
succ X);
set FY = (
FlatPoset Y);
set CY = (
succ Y);
reconsider h1, h2 as
continuous
Function of FX, FY by
A00;
for g1,g2 be
continuous
Function of FX, FY st ((for x be
Element of FX, f1,f2 be
continuous
Function of FX, FY st h1
= f1 & h2
= f2 holds (g1
. x)
= (
BaseFunc02 (x,(f1
. ((
Flatten E1)
. x)),(f2
. ((
Flatten E2)
. x)),I,J,D))) & (for x be
Element of FX, f1,f2 be
continuous
Function of FX, FY st h1
= f1 & h2
= f2 holds (g2
. x)
= (
BaseFunc02 (x,(f1
. ((
Flatten E1)
. x)),(f2
. ((
Flatten E2)
. x)),I,J,D)))) holds g1
= g2
proof
let g1,g2 be
continuous
Function of FX, FY;
assume
B1: (for x be
Element of FX, f1,f2 be
continuous
Function of FX, FY st h1
= f1 & h2
= f2 holds (g1
. x)
= (
BaseFunc02 (x,(f1
. ((
Flatten E1)
. x)),(f2
. ((
Flatten E2)
. x)),I,J,D))) & (for x be
Element of FX, f1,f2 be
continuous
Function of FX, FY st h1
= f1 & h2
= f2 holds (g2
. x)
= (
BaseFunc02 (x,(f1
. ((
Flatten E1)
. x)),(f2
. ((
Flatten E2)
. x)),I,J,D)));
for x be
Element of FX holds (g1
. x)
= (g2
. x)
proof
let x be
Element of FX;
(g1
. x)
= (
BaseFunc02 (x,(h1
. ((
Flatten E1)
. x)),(h2
. ((
Flatten E2)
. x)),I,J,D)) by
B1
.= (g2
. x) by
B1;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
end
theorem ::
POSET_2:23
Threcursive0101: ex W be
continuous
Function of
[:(
FlatConF (X,Y)), (
FlatConF (X,Y)):], (
FlatConF (X,Y)) st for f be
set st f
in
[:(
ConFuncs ((
FlatPoset X),(
FlatPoset Y))), (
ConFuncs ((
FlatPoset X),(
FlatPoset Y))):] holds (W
. f)
= (
RecFunc02 ((f
`1 ),(f
`2 ),E1,E2,I,J,D))
proof
set FX = (
FlatPoset X);
set CX = (
succ X);
set FY = (
FlatPoset Y);
set CY = (
succ Y);
set FlatC = (
FlatConF (X,Y));
set CFXY = (
ConFuncs (FX,FY));
set CRFXY = (
ConRelat (FX,FY));
set FlatC2 =
[:FlatC, FlatC:];
set CFXY2 =
[:CFXY, CFXY:];
set CRFXY2 =
["CRFXY, CRFXY"];
A6: the
carrier of FlatC2
= CFXY2 & the
InternalRel of FlatC2
= CRFXY2 by
YELLOW_3:def 2;
deffunc
H(
object) = (
RecFunc02 (($1
`1 ),($1
`2 ),E1,E2,I,J,D));
A7: for h be
continuous
Function of FX, FY holds h
in CFXY
proof
let h be
continuous
Function of FX, FY;
h
in (
Funcs (the
carrier of FX,the
carrier of FY)) by
FUNCT_2: 8;
hence thesis;
end;
A8: for h be
set st h
in CFXY holds h is
continuous
Function of FX, FY
proof
let h be
set;
assume h
in CFXY;
then
consider x be
Element of (
Funcs (the
carrier of FX,the
carrier of FY)) such that
B1: h
= x & ex g be
continuous
Function of FX, FY st g
= x;
thus thesis by
B1;
end;
A801: for h be
Element of FlatC2 holds ex h1,h2 be
continuous
Function of FX, FY st h
=
[h1, h2]
proof
let h be
Element of FlatC2;
B1: h is
Element of CFXY2 by
YELLOW_3:def 2;
reconsider h1 = (h
`1 ), h2 = (h
`2 ) as
continuous
Function of FX, FY by
A8;
take h1, h2;
consider xx,y be
object such that
hh: xx
in CFXY & y
in CFXY & h
=
[xx, y] by
ZFMISC_1:def 2,
B1;
thus thesis by
hh;
end;
A9: for f be
object st f
in CFXY2 holds
H(f)
in CFXY by
A7;
ex W be
Function of CFXY2, CFXY st for f be
object st f
in CFXY2 holds (W
. f)
=
H(f) from
FUNCT_2:sch 2(
A9);
then
consider IT be
Function of CFXY2, CFXY such that
A10: for f be
object st f
in CFXY2 holds (IT
. f)
=
H(f);
IT is
continuous
Function of FlatC2, FlatC
proof
B1: for f1,f2 be
continuous
Function of FX, FY holds (IT
.
[f1, f2])
=
H([)
proof
let f1,f2 be
continuous
Function of FX, FY;
set f =
[f1, f2];
f1
in CFXY & f2
in CFXY by
A7;
then f
in CFXY2 by
ZFMISC_1:def 2;
hence thesis by
A10;
end;
B2: for f1,f2 be
continuous
Function of FX, FY holds ex g be
continuous
Function of FX, FY st g
= (IT
.
[f1, f2])
proof
let f1,f2 be
continuous
Function of FX, FY;
set f =
[f1, f2];
f1
in CFXY & f2
in CFXY by
A7;
then
C1: f
in CFXY2 by
ZFMISC_1:def 2;
reconsider g = (IT
. f) as
continuous
Function of FX, FY by
A8,
C1,
FUNCT_2: 5;
take g;
thus thesis;
end;
B3: for f1,f2 be
continuous
Function of FX, FY holds for g be
continuous
Function of FX, FY st g
= (IT
.
[f1, f2]) holds for x be
Element of FX holds (((g
. x)
= (
BaseFunc02 (x,(f1
. ((
Flatten E1)
. x)),(f2
. ((
Flatten E2)
. x)),I,J,D))) & (x
in D implies (g
. x)
= (I
. x)))
proof
let f1,f2 be
continuous
Function of FX, FY;
let g be
continuous
Function of FX, FY;
assume
C1: g
= (IT
.
[f1, f2]);
let x be
Element of FX;
(
[f1, f2]
`1 )
= f1 & (
[f1, f2]
`2 )
= f2;
then (g
. x)
= ((
RecFunc02 (f1,f2,E1,E2,I,J,D))
. x) by
B1,
C1
.= (
BaseFunc02 (x,(f1
. ((
Flatten E1)
. x)),(f2
. ((
Flatten E2)
. x)),I,J,D)) by
DefRecFunc02;
hence thesis by
DefBaseFunc02;
end;
reconsider IT as
Function of FlatC2, FlatC by
A6;
IT is
monotone
proof
let f1,f2 be
Element of FlatC2 such that
C1: f1
<= f2;
let g1,g2 be
Element of FlatC such that
C2: g1
= (IT
. f1) & g2
= (IT
. f2);
reconsider f101 = (f1
`1 ), f102 = (f1
`2 ), f201 = (f2
`1 ), f202 = (f2
`2 ) as
Element of FlatC;
[f101, f201]
in CRFXY by
ORDERS_2:def 5,
C1,
YELLOW_3: 12;
then
consider f1011,f2011 be
Function of FX, FY such that
C301: f101
= f1011 & f201
= f2011 & f1011
<= f2011 by
POSET_1:def 7;
reconsider f1011, f2011 as
continuous
Function of FX, FY by
C301,
A8;
[f102, f202]
in CRFXY by
ORDERS_2:def 5,
C1,
YELLOW_3: 12;
then
consider f1021,f2021 be
Function of FX, FY such that
C401: f102
= f1021 & f202
= f2021 & f1021
<= f2021 by
POSET_1:def 7;
reconsider f1021, f2021 as
continuous
Function of FX, FY by
C401,
A8;
reconsider g10 = g1, g20 = g2 as
continuous
Function of FX, FY by
A8;
for x be
Element of FX holds (g10
. x)
<= (g20
. x)
proof
let x be
Element of FX;
reconsider y01 = ((
Flatten E1)
. x), y02 = ((
Flatten E2)
. x) as
Element of FX;
set y1 = (f1011
. y01);
set y2 = (f2011
. y01);
set y3 = (f1021
. y02);
set y4 = (f2021
. y02);
f1
in the
carrier of
[:FlatC, FlatC:];
then f1
in
[:the
carrier of FlatC, the
carrier of FlatC:] by
YELLOW_3:def 2;
then
consider xx,y be
object such that
hh: xx
in the
carrier of FlatC & y
in the
carrier of FlatC & f1
=
[xx, y] by
ZFMISC_1:def 2;
D1: g10
= (IT
.
[f1011, f1021]) by
C2,
C401,
hh,
C301;
D101: (g10
. x)
= (
BaseFunc02 (x,y1,y3,I,J,D)) by
B3,
C2,
C401,
hh,
C301;
f2
in the
carrier of
[:FlatC, FlatC:];
then f2
in
[:the
carrier of FlatC, the
carrier of FlatC:] by
YELLOW_3:def 2;
then
consider xx,y be
object such that
hh: xx
in the
carrier of FlatC & y
in the
carrier of FlatC & f2
=
[xx, y] by
ZFMISC_1:def 2;
D2: g20
= (IT
.
[f2011, f2021]) by
C2,
C401,
C301,
hh;
per cases by
ThFlatten04,
C301,
YELLOW_2: 9;
suppose y1
= Y;
then
D301: not y1
in Y;
per cases ;
suppose
D302: x
in D;
then (g10
. x)
= (I
. x) by
D1,
B3;
hence thesis by
D2,
B3,
D302;
end;
suppose not x
in D;
then (g10
. x)
= Y by
D301,
D101,
DefBaseFunc02;
hence thesis by
LemFlatten02;
end;
end;
suppose
D304: y1
= y2;
per cases by
C401,
YELLOW_2: 9,
ThFlatten04;
suppose y3
= Y;
then
D305: not y3
in Y;
per cases ;
suppose
D306: x
in D;
then (g10
. x)
= (I
. x) by
D1,
B3;
hence thesis by
D2,
B3,
D306;
end;
suppose not x
in D;
then (g10
. x)
= Y by
D305,
D101,
DefBaseFunc02;
hence thesis by
LemFlatten02;
end;
end;
suppose y3
= y4;
hence thesis by
D101,
C2,
C401,
C301,
hh,
B3,
D304;
end;
end;
end;
then g10
<= g20 by
YELLOW_2: 9;
hence thesis by
POSET_1:def 7;
end;
then
reconsider IT as
monotone
Function of FlatC2, FlatC;
for F be non
empty
Chain of FlatC2 holds (IT
. (
sup F))
<= (
sup (IT
.: F))
proof
let F be non
empty
Chain of FlatC2;
reconsider G = (IT
.: F) as non
empty
Chain of FlatC by
POSET_1: 1;
(IT
. (
sup F))
<= (
sup G)
proof
reconsider F as non
empty
Chain of
[:(
ConPoset (FX,FY)), (
ConPoset (FX,FY)):];
reconsider G as non
empty
Chain of (
ConPoset (FX,FY));
D101: (
sup (
proj1 F))
= (
sup_func (
proj1 F)) by
POSET_1: 11;
then
reconsider sf1 = (
sup (
proj1 F)) as
continuous
Function of FX, FY;
D102: (
sup (
proj2 F))
= (
sup_func (
proj2 F)) by
POSET_1: 11;
then
reconsider sf2 = (
sup (
proj2 F)) as
continuous
Function of FX, FY;
D103: (
sup F)
=
[sf1, sf2] by
YELLOW_3: 46,
LemProdPoset06;
set sg = (
sup G);
D3: sg
= (
sup_func G) by
POSET_1: 11;
then
reconsider sg as
continuous
Function of FX, FY;
D4: for x be
Element of FX st x
in D holds (sg
. x)
= (I
. x)
proof
let x be
Element of FX;
assume
D401: x
in D;
reconsider N = (G
-image x) as non
empty
Chain of FY;
set h = the
Element of G;
reconsider h as
continuous
Function of FX, FY by
A8;
reconsider hx = (h
. x) as
Element of FY;
D402: hx
in N;
consider f be
Element of CFXY2 such that
D403: f
in F & h
= (IT
. f) by
FUNCT_2: 65;
reconsider f as
Element of FlatC2 by
D403;
consider f1,f2 be
continuous
Function of FX, FY such that
D404: f
=
[f1, f2] by
A801;
D405: hx
= (I
. x) by
B3,
D401,
D403,
D404;
then hx
in Y by
FUNCT_2: 5,
D401;
then hx
<> Y;
then (
sup N)
= hx by
ThFlatten04,
D402,
Thsup01;
hence thesis by
D405,
POSET_1:def 10,
D3;
end;
consider g be
continuous
Function of FX, FY such that
D5: g
= (IT
.
[sf1, sf2]) by
B2;
for x be
Element of FX holds (g
. x)
<= (sg
. x)
proof
let x be
Element of FX;
reconsider x1 = ((
Flatten E1)
. x), x2 = ((
Flatten E2)
. x) as
Element of FX;
reconsider M1 = ((
proj1 F)
-image x1), M2 = ((
proj2 F)
-image x2) as non
empty
Chain of FY;
consider a1 be
Element of FY such that
E401: M1
=
{a1} or M1
=
{(
Bottom FY), a1} by
Thflat01;
E402: (
sup M1)
= a1
proof
per cases by
E401;
suppose M1
=
{a1};
hence thesis by
YELLOW_0: 39;
end;
suppose M1
=
{(
Bottom FY), a1};
hence thesis by
Thflat0502;
end;
end;
consider a2 be
Element of FY such that
E403: M2
=
{a2} or M2
=
{(
Bottom FY), a2} by
Thflat01;
E404: (
sup M2)
= a2
proof
per cases by
E403;
suppose M2
=
{a2};
hence thesis by
YELLOW_0: 39;
end;
suppose M2
=
{(
Bottom FY), a2};
hence thesis by
Thflat0502;
end;
end;
E0: (sf1
. x1)
= a1 & (sf2
. x2)
= a2 by
POSET_1:def 10,
D101,
D102,
E402,
E404;
E1: (g
. x)
= (
BaseFunc02 (x,a1,a2,I,J,D)) by
B3,
D5,
E0;
E500: a1
in ((
proj1 F)
-image x1) & a2
in ((
proj2 F)
-image x2) by
TARSKI:def 1,
TARSKI:def 2,
E401,
E403;
consider q1 be
Element of FY such that
E501: q1
= a1 & ex f1 be
continuous
Function of FX, FY st f1
in (
proj1 F) & q1
= (f1
. x1) by
E500;
consider q2 be
Element of FY such that
E502: q2
= a2 & ex f2 be
continuous
Function of FX, FY st f2
in (
proj2 F) & q2
= (f2
. x2) by
E500;
per cases ;
suppose
E503: not x
in D;
per cases ;
suppose
E504: a1
<> Y & a2
<> Y;
ex f1,f2 be
continuous
Function of FX, FY st
[f1, f2]
in F & a1
= (f1
. x1) & a2
= (f2
. x2)
proof
consider f1,f2 be
continuous
Function of FX, FY such that
E600: f1
in (
proj1 F) & a1
= (f1
. x1) & f2
in (
proj2 F) & a2
= (f2
. x2) by
E501,
E502;
consider f12 be
object such that
E601:
[f1, f12]
in F by
E600,
XTUPLE_0:def 12;
(
[f1, f12]
`2 )
in CFXY by
MCART_1: 10,
A6,
E601;
then
reconsider f12 as
continuous
Function of FX, FY by
A8;
consider f21 be
object such that
E602:
[f21, f2]
in F by
E600,
XTUPLE_0:def 13;
(
[f21, f2]
`1 )
in CFXY by
MCART_1: 10,
A6,
E602;
then
reconsider f21 as
continuous
Function of FX, FY by
A8;
reconsider f1F = f1, f12F = f12, f2F = f2, f21F = f21 as
Element of FlatC by
A7;
reconsider h1 =
[f1F, f12F], h2 =
[f21F, f2F] as
Element of F by
E601,
E602;
reconsider h1, h2 as
Element of FlatC2;
per cases by
ORDERS_2: 11;
suppose h1
<= h2;
then f1F
<= f21F by
YELLOW_3: 11;
then
consider f,g be
Function of FX, FY such that
G001: f1
= f & f21
= g & f
<= g by
POSET_1:def 7;
take f21, f2;
thus thesis by
E602,
E600,
E504,
ThFlatten04,
YELLOW_2: 9,
G001;
end;
suppose h2
<= h1;
then f2F
<= f12F by
YELLOW_3: 11;
then
consider f,g be
Function of FX, FY such that
G001: f2
= f & f12
= g & f
<= g by
POSET_1:def 7;
take f1, f12;
thus thesis by
E601,
E600,
E504,
ThFlatten04,
YELLOW_2: 9,
G001;
end;
end;
then
consider f1,f2 be
continuous
Function of FX, FY such that
E6:
[f1, f2]
in F & a1
= (f1
. x1) & a2
= (f2
. x2);
f1
in CFXY & f2
in CFXY by
A7;
then
reconsider f01 =
[f1, f2] as
Element of FlatC2 by
ZFMISC_1:def 2,
A6;
reconsider g01 = (IT
. f01) as
continuous
Function of FX, FY by
A8;
E7: (g01
. x)
= (g
. x) by
B3,
E6,
E1;
reconsider N = (G
-image x) as non
empty
Chain of FY;
E9: (sg
. x)
= (
sup N) by
POSET_1:def 10,
D3;
(
dom IT)
= CFXY2 by
FUNCT_2:def 1;
then
[f01, g01]
in IT by
FUNCT_1:def 2,
A6;
then g01
in (IT
.: F) by
RELAT_1:def 13,
E6;
then (g01
. x)
in N;
hence thesis by
E7,
Thsup01,
E9;
end;
suppose a1
= Y or a2
= Y;
then not (a1
in Y & a2
in Y);
then (g
. x)
= Y by
E1,
DefBaseFunc02,
E503;
hence thesis by
LemFlatten02;
end;
end;
suppose
E506: x
in D;
then (sg
. x)
= (I
. x) by
D4
.= (g
. x) by
E506,
B3,
D5;
hence thesis;
end;
end;
then g
<= sg by
YELLOW_2: 9;
hence thesis by
D5,
D103,
POSET_1:def 7;
end;
hence thesis;
end;
hence thesis by
POSET_1: 8;
end;
then
reconsider IT as
continuous
Function of FlatC2, FlatC;
for f be
set st f
in CFXY2 holds (IT
. f)
= (
RecFunc02 ((f
`1 ),(f
`2 ),E1,E2,I,J,D)) by
A10;
hence thesis;
end;
theorem ::
POSET_2:24
Threcursive0201: ex f,g be
set st f
in (
ConFuncs ((
FlatPoset X),(
FlatPoset Y))) & g
in (
ConFuncs ((
FlatPoset X),(
FlatPoset Y))) & f
= (
RecFunc02 (f,g,E1,E2,I1,J1,D)) & g
= (
RecFunc02 (f,g,E1,E2,I2,J2,D))
proof
set FX = (
FlatPoset X);
set FY = (
FlatPoset Y);
set FlatC = (
FlatConF (X,Y));
set CFXY = (
ConFuncs (FX,FY));
set CRFXY = (
ConRelat (FX,FY));
set FlatC2 =
[:FlatC, FlatC:];
set CFXY2 =
[:CFXY, CFXY:];
set CRFXY2 =
["CRFXY, CRFXY"];
A4: the
carrier of FlatC2
= CFXY2 & the
InternalRel of FlatC2
= CRFXY2 by
YELLOW_3:def 2;
consider W1 be
continuous
Function of FlatC2, FlatC such that
A5: for h be
set st h
in CFXY2 holds (W1
. h)
= (
RecFunc02 ((h
`1 ),(h
`2 ),E1,E2,I1,J1,D)) by
Threcursive0101;
consider W2 be
continuous
Function of FlatC2, FlatC such that
A6: for h be
set st h
in CFXY2 holds (W2
. h)
= (
RecFunc02 ((h
`1 ),(h
`2 ),E1,E2,I2,J2,D)) by
Threcursive0101;
reconsider W =
<:W1, W2:> as
continuous
Function of FlatC2, FlatC2 by
YELLOW_3:def 2;
reconsider h = (
least_fix_point W) as
Element of FlatC2;
h
is_a_fixpoint_of W by
POSET_1:def 5;
then
A7: h
= (W
. h) by
ABIAN:def 3;
A8: (W1
. h)
= (
RecFunc02 ((h
`1 ),(h
`2 ),E1,E2,I1,J1,D)) & (W2
. h)
= (
RecFunc02 ((h
`1 ),(h
`2 ),E1,E2,I2,J2,D)) by
A4,
A5,
A6;
consider f,g be
Element of FlatC such that
A9: h
=
[f, g] by
ThProdPoset01;
take f, g;
(
dom W)
= the
carrier of FlatC2 by
FUNCT_2:def 1;
then
[f, g]
=
[(
RecFunc02 (f,g,E1,E2,I1,J1,D)), (
RecFunc02 (f,g,E1,E2,I2,J2,D))] by
FUNCT_3:def 7,
A7,
A8,
A9;
hence thesis by
XTUPLE_0: 1;
end;
theorem ::
POSET_2:25
Threcursive0301: (E1,E2)
is_well_founded_with_minimal_set D implies ex f,g be
continuous
Function of (
FlatPoset X), (
FlatPoset Y) st for x be
Element of X holds ((f
. x)
in Y & (f
. x)
= (
BaseFunc02 (x,(f
. (E1
. x)),(g
. (E2
. x)),I1,J1,D)) & (g
. x)
in Y & (g
. x)
= (
BaseFunc02 (x,(f
. (E1
. x)),(g
. (E2
. x)),I2,J2,D)))
proof
assume
A1: (E1,E2)
is_well_founded_with_minimal_set D;
A2: not X
in X & not Y
in Y;
set FX = (
FlatPoset X);
set CX = (
succ X);
set FY = (
FlatPoset Y);
set CY = (
succ Y);
consider f,g be
set such that
A7: f
in (
ConFuncs ((
FlatPoset X),(
FlatPoset Y))) & g
in (
ConFuncs ((
FlatPoset X),(
FlatPoset Y))) & f
= (
RecFunc02 (f,g,E1,E2,I1,J1,D)) & g
= (
RecFunc02 (f,g,E1,E2,I2,J2,D)) by
Threcursive0201;
reconsider f, g as
continuous
Function of (
FlatPoset X), (
FlatPoset Y) by
A7;
take f, g;
consider l be
Function of X,
NAT such that
A801: for x0 be
Element of X holds ((l
. x0)
<=
0 implies x0
in D) & ( not x0
in D implies (l
. (E1
. x0))
< (l
. x0) & (l
. (E2
. x0))
< (l
. x0)) by
A1;
defpred
P[
Nat] means for x1,x2 be
Element of X st (l
. x1)
<= $1 & (l
. x2)
<= $1 holds ((f
. x1)
in Y & (f
. x1)
= (
BaseFunc02 (x1,(f
. (E1
. x1)),(g
. (E2
. x1)),I1,J1,D)) & (g
. x2)
in Y & (g
. x2)
= (
BaseFunc02 (x2,(f
. (E1
. x2)),(g
. (E2
. x2)),I2,J2,D)));
A9:
P[
0 ]
proof
let x1,x2 be
Element of X;
assume
b1: (l
. x1)
<=
0 & (l
. x2)
<=
0 ;
B2: x1
in X & x2
in X;
reconsider x1, x2 as
Element of FX by
XBOOLE_0:def 3;
x1
<> X & x2
<> X by
B2;
then
B4: (f
. ((
Flatten E1)
. x1))
= (f
. (E1
. x1)) & (g
. ((
Flatten E2)
. x1))
= (g
. (E2
. x1)) & (f
. ((
Flatten E1)
. x2))
= (f
. (E1
. x2)) & (g
. ((
Flatten E2)
. x2))
= (g
. (E2
. x2)) by
DefFlatten04;
(f
. x1)
= (
BaseFunc02 (x1,(f
. (E1
. x1)),(g
. (E2
. x1)),I1,J1,D)) by
A7,
DefRecFunc02,
B4;
then
B6: (f
. x1)
= (I1
. x1) by
DefBaseFunc02,
b1,
A801;
(g
. x2)
= (
BaseFunc02 (x2,(f
. (E1
. x2)),(g
. (E2
. x2)),I2,J2,D)) by
A7,
DefRecFunc02,
B4;
then (g
. x2)
= (I2
. x2) by
DefBaseFunc02,
b1,
A801;
hence thesis by
A7,
DefRecFunc02,
B4,
FUNCT_2: 5,
B6;
end;
A10: for k st
P[k] holds
P[(k
+ 1)]
proof
let k;
assume
B0:
P[k];
let x01,x02 be
Element of X;
assume
B1: (l
. x01)
<= (k
+ 1) & (l
. x02)
<= (k
+ 1);
reconsider x01, x02 as
Element of FX by
XBOOLE_0:def 3;
x01
<> X & x02
<> X by
A2;
then
B4: (f
. ((
Flatten E1)
. x01))
= (f
. (E1
. x01)) & (g
. ((
Flatten E2)
. x01))
= (g
. (E2
. x01)) & (f
. ((
Flatten E1)
. x02))
= (f
. (E1
. x02)) & (g
. ((
Flatten E2)
. x02))
= (g
. (E2
. x02)) by
DefFlatten04;
set x11 = (E1
. x01);
set x21 = (E2
. x01);
set x12 = (E1
. x02);
set x22 = (E2
. x02);
reconsider x11, x12, x21, x22 as
Element of X by
FUNCT_2: 5;
B501: (f
. x01)
= (
BaseFunc02 (x01,(f
. x11),(g
. x21),I1,J1,D)) by
A7,
DefRecFunc02,
B4;
B502: (g
. x02)
= (
BaseFunc02 (x02,(f
. x12),(g
. x22),I2,J2,D)) by
A7,
DefRecFunc02,
B4;
reconsider x01, x02 as
Element of X;
per cases ;
suppose x01
in D;
then
C2: (f
. x01)
= (I1
. x01) by
DefBaseFunc02,
B501;
per cases ;
suppose x02
in D;
then (g
. x02)
= (I2
. x02) by
DefBaseFunc02,
B502;
hence thesis by
C2,
A7,
DefRecFunc02,
B4;
end;
suppose
C01: not x02
in D;
then ((l
. x12)
+ 1)
<= (l
. x02) & ((l
. x22)
+ 1)
<= (l
. x02) by
NAT_1: 13,
A801;
then ((l
. x12)
+ 1)
<= (k
+ 1) & ((l
. x22)
+ 1)
<= (k
+ 1) by
B1,
XXREAL_0: 2;
then (l
. x12)
<= k & (l
. x22)
<= k by
XREAL_1: 8;
then
C04: (f
. x12)
in Y & (g
. x22)
in Y by
B0;
C06: (g
. x02)
= (J2
.
[x02, (f
. x12), (g
. x22)]) by
B502,
DefBaseFunc02,
C01,
C04;
[x02, (f
. x12), (g
. x22)]
in
[:X, Y, Y:] by
C04,
MCART_1: 69;
hence thesis by
C2,
C06,
A7,
DefRecFunc02,
B4,
FUNCT_2: 5;
end;
end;
suppose
C1: not x01
in D;
then ((l
. x11)
+ 1)
<= (l
. x01) & ((l
. x21)
+ 1)
<= (l
. x01) by
NAT_1: 13,
A801;
then ((l
. x11)
+ 1)
<= (k
+ 1) & ((l
. x21)
+ 1)
<= (k
+ 1) by
B1,
XXREAL_0: 2;
then (l
. x11)
<= k & (l
. x21)
<= k by
XREAL_1: 8;
then
C4: (f
. x11)
in Y & (g
. x21)
in Y by
B0;
then
C6: (f
. x01)
= (J1
.
[x01, (f
. x11), (g
. x21)]) by
B501,
DefBaseFunc02,
C1;
C7:
[x01, (f
. x11), (g
. x21)]
in
[:X, Y, Y:] by
C4,
MCART_1: 69;
per cases ;
suppose x02
in D;
then (g
. x02)
= (I2
. x02) by
DefBaseFunc02,
B502;
hence thesis by
C6,
C7,
FUNCT_2: 5,
A7,
DefRecFunc02,
B4;
end;
suppose
C01: not x02
in D;
then ((l
. x12)
+ 1)
<= (l
. x02) & ((l
. x22)
+ 1)
<= (l
. x02) by
NAT_1: 13,
A801;
then ((l
. x12)
+ 1)
<= (k
+ 1) & ((l
. x22)
+ 1)
<= (k
+ 1) by
B1,
XXREAL_0: 2;
then (l
. x12)
<= k & (l
. x22)
<= k by
XREAL_1: 8;
then
C04: (f
. x12)
in Y & (g
. x22)
in Y by
B0;
C06: (g
. x02)
= (J2
.
[x02, (f
. x12), (g
. x22)]) by
B502,
DefBaseFunc02,
C01,
C04;
[x02, (f
. x12), (g
. x22)]
in
[:X, Y, Y:] by
C04,
MCART_1: 69;
hence thesis by
C6,
C7,
C06,
A7,
DefRecFunc02,
B4,
FUNCT_2: 5;
end;
end;
end;
A11: for k be
Nat holds
P[k] from
NAT_1:sch 2(
A9,
A10);
for x1,x2 be
Element of X holds (f
. x1)
in Y & (f
. x1)
= (
BaseFunc02 (x1,(f
. (E1
. x1)),(g
. (E2
. x1)),I1,J1,D)) & (g
. x2)
in Y & (g
. x2)
= (
BaseFunc02 (x2,(f
. (E1
. x2)),(g
. (E2
. x2)),I2,J2,D))
proof
let x1,x2 be
Element of X;
reconsider k = ((l
. x1)
+ (l
. x2)) as
Nat;
(l
. x1)
<= k & (l
. x2)
<= k by
NAT_1: 11;
hence thesis by
A11;
end;
hence thesis;
end;
Lemrecursive0401: (E1,E2)
is_well_founded_with_minimal_set D implies ex f,g be
Function of X, Y st for x be
Element of X holds (f
. x)
= (
BaseFunc02 (x,(f
. (E1
. x)),(g
. (E2
. x)),I1,J1,D)) & (g
. x)
= (
BaseFunc02 (x,(f
. (E1
. x)),(g
. (E2
. x)),I2,J2,D))
proof
assume
A1: (E1,E2)
is_well_founded_with_minimal_set D;
set FX = (
FlatPoset X);
set CX = (
succ X);
A02: X
c= CX by
XBOOLE_1: 7;
set FY = (
FlatPoset Y);
set CY = (
succ Y);
consider f,g be
continuous
Function of FX, FY such that
A3: for x be
Element of X holds ((f
. x)
in Y & (f
. x)
= (
BaseFunc02 (x,(f
. (E1
. x)),(g
. (E2
. x)),I1,J1,D)) & (g
. x)
in Y & (g
. x)
= (
BaseFunc02 (x,(f
. (E1
. x)),(g
. (E2
. x)),I2,J2,D))) by
A1,
Threcursive0301;
reconsider f, g as
Function of CX, CY;
reconsider fX = (f
| X), gX = (g
| X) as
Function of X, CY by
A02,
FUNCT_2: 32;
for x be
Element of X holds (fX
. x)
in Y & (gX
. x)
in Y
proof
let x be
Element of X;
(f
. x)
in Y & (g
. x)
in Y by
A3;
hence thesis by
FUNCT_1: 49;
end;
then (
rng fX)
c= Y & (
rng gX)
c= Y by
FUNCT_2: 114;
then
reconsider fX, gX as
Function of X, Y by
FUNCT_2: 6;
take fX, gX;
let x be
Element of X;
reconsider x1 = (E1
. x), x2 = (E2
. x) as
Element of X;
B2: (fX
. x1)
= (f
. x1) & (gX
. x2)
= (g
. x2) by
FUNCT_1: 49;
B3: (fX
. x)
= (f
. x) by
FUNCT_1: 49
.= (
BaseFunc02 (x,(fX
. x1),(gX
. x2),I1,J1,D)) by
A3,
B2;
(gX
. x)
= (g
. x) by
FUNCT_1: 49
.= (
BaseFunc02 (x,(f
. x1),(g
. x2),I2,J2,D)) by
A3;
hence thesis by
B2,
B3;
end;
theorem ::
POSET_2:26
Threcursive05: (E1,E2)
is_well_founded_with_minimal_set D implies ex f,g be
Function of X, Y st for x be
Element of X holds (x
in D implies (f
. x)
= (I1
. x) & (g
. x)
= (I2
. x)) & ( not x
in D implies (f
. x)
= (J1
.
[x, (f
. (E1
. x)), (g
. (E2
. x))]) & (g
. x)
= (J2
.
[x, (f
. (E1
. x)), (g
. (E2
. x))]))
proof
assume (E1,E2)
is_well_founded_with_minimal_set D;
then
consider f,g be
Function of X, Y such that
A1: for x be
Element of X holds (f
. x)
= (
BaseFunc02 (x,(f
. (E1
. x)),(g
. (E2
. x)),I1,J1,D)) & (g
. x)
= (
BaseFunc02 (x,(f
. (E1
. x)),(g
. (E2
. x)),I2,J2,D)) by
Lemrecursive0401;
take f, g;
let x be
Element of X;
(f
. x)
= (
BaseFunc02 (x,(f
. (E1
. x)),(g
. (E2
. x)),I1,J1,D)) & (g
. x)
= (
BaseFunc02 (x,(f
. (E1
. x)),(g
. (E2
. x)),I2,J2,D)) by
A1;
hence thesis by
DefBaseFunc02;
end;
theorem ::
POSET_2:27
for f1,g1,f2,g2 be
Function of X, Y holds (E1,E2)
is_well_founded_with_minimal_set D & (for x be
Element of X holds (x
in D implies (f1
. x)
= (I1
. x) & (g1
. x)
= (I2
. x)) & ( not x
in D implies (f1
. x)
= (J1
.
[x, (f1
. (E1
. x)), (g1
. (E2
. x))]) & (g1
. x)
= (J2
.
[x, (f1
. (E1
. x)), (g1
. (E2
. x))]))) & (for x be
Element of X holds (x
in D implies (f2
. x)
= (I1
. x) & (g2
. x)
= (I2
. x)) & ( not x
in D implies (f2
. x)
= (J1
.
[x, (f2
. (E1
. x)), (g2
. (E2
. x))]) & (g2
. x)
= (J2
.
[x, (f2
. (E1
. x)), (g2
. (E2
. x))]))) implies f1
= f2 & g1
= g2
proof
let f1,g1,f2,g2 be
Function of X, Y;
assume
A0: (E1,E2)
is_well_founded_with_minimal_set D & (for x be
Element of X holds (x
in D implies (f1
. x)
= (I1
. x) & (g1
. x)
= (I2
. x)) & ( not x
in D implies (f1
. x)
= (J1
.
[x, (f1
. (E1
. x)), (g1
. (E2
. x))]) & (g1
. x)
= (J2
.
[x, (f1
. (E1
. x)), (g1
. (E2
. x))]))) & (for x be
Element of X holds (x
in D implies (f2
. x)
= (I1
. x) & (g2
. x)
= (I2
. x)) & ( not x
in D implies (f2
. x)
= (J1
.
[x, (f2
. (E1
. x)), (g2
. (E2
. x))]) & (g2
. x)
= (J2
.
[x, (f2
. (E1
. x)), (g2
. (E2
. x))])));
then
consider l be
Function of X,
NAT such that
A1: for x be
Element of X holds ((l
. x)
<=
0 implies x
in D) & ( not x
in D implies (l
. (E1
. x))
< (l
. x) & (l
. (E2
. x))
< (l
. x));
defpred
P[
Nat] means for x be
Element of X st (l
. x)
<= $1 holds (f1
. x)
= (f2
. x) & (g1
. x)
= (g2
. x);
A2:
P[
0 ]
proof
let x be
Element of X;
assume (l
. x)
<=
0 ;
then
B1: x
in D by
A1;
B2: (f1
. x)
= (I1
. x) by
A0,
B1
.= (f2
. x) by
A0,
B1;
(g1
. x)
= (I2
. x) by
A0,
B1
.= (g2
. x) by
A0,
B1;
hence thesis by
B2;
end;
A3: for k st
P[k] holds
P[(k
+ 1)]
proof
let k;
assume
B0:
P[k];
let x be
Element of X;
assume
B1: (l
. x)
<= (k
+ 1);
per cases ;
suppose
C0: x
in D;
C1: (f1
. x)
= (I1
. x) by
A0,
C0
.= (f2
. x) by
A0,
C0;
(g1
. x)
= (I2
. x) by
A0,
C0
.= (g2
. x) by
A0,
C0;
hence thesis by
C1;
end;
suppose
C0: not x
in D;
reconsider x1 = (E1
. x), x2 = (E2
. x) as
Element of X;
((l
. x1)
+ 1)
<= (l
. x) & ((l
. x2)
+ 1)
<= (l
. x) by
NAT_1: 13,
A1,
C0;
then ((l
. x1)
+ 1)
<= (k
+ 1) & ((l
. x2)
+ 1)
<= (k
+ 1) by
B1,
XXREAL_0: 2;
then (l
. x1)
<= k & (l
. x2)
<= k by
XREAL_1: 8;
then
C1: (f1
. x1)
= (f2
. x1) & (g1
. x2)
= (g2
. x2) by
B0;
C2: (f1
. x)
= (J1
.
[x, (f2
. x1), (g2
. x2)]) by
A0,
C0,
C1
.= (f2
. x) by
A0,
C0;
(g1
. x)
= (J2
.
[x, (f2
. x1), (g2
. x2)]) by
A0,
C0,
C1
.= (g2
. x) by
A0,
C0;
hence thesis by
C2;
end;
end;
A4: for k be
Nat holds
P[k] from
NAT_1:sch 2(
A2,
A3);
for x be
Element of X holds (f1
. x)
= (f2
. x) & (g1
. x)
= (g2
. x)
proof
let x be
Element of X;
reconsider k = (l
. x) as
Nat;
(l
. x)
<= k;
hence thesis by
A4;
end;
hence thesis;
end;
theorem ::
POSET_2:28
(E1,E2)
is_well_founded_with_minimal_set D implies ex f be
Function of X, Y st for x be
Element of X holds (x
in D implies (f
. x)
= (I
. x)) & ( not x
in D implies (f
. x)
= (J
.
[x, (f
. (E1
. x)), (f
. (E2
. x))]))
proof
assume (E1,E2)
is_well_founded_with_minimal_set D;
then
consider f,g be
Function of X, Y such that
A1: for x be
Element of X holds (x
in D implies (f
. x)
= (I
. x) & (g
. x)
= (I
. x)) & ( not x
in D implies (f
. x)
= (J
.
[x, (f
. (E1
. x)), (g
. (E2
. x))]) & (g
. x)
= (J
.
[x, (f
. (E1
. x)), (g
. (E2
. x))])) by
Threcursive05;
for x be
Element of X holds (f
. x)
= (g
. x)
proof
let x be
Element of X;
per cases ;
suppose
C0: x
in D;
then (f
. x)
= (I
. x) by
A1
.= (g
. x) by
A1,
C0;
hence thesis;
end;
suppose
C0: not x
in D;
then (f
. x)
= (J
.
[x, (f
. (E1
. x)), (g
. (E2
. x))]) by
A1
.= (g
. x) by
A1,
C0;
hence thesis;
end;
end;
then f
= g;
then for x be
Element of X holds (x
in D implies (f
. x)
= (I
. x)) & ( not x
in D implies (f
. x)
= (J
.
[x, (f
. (E1
. x)), (f
. (E2
. x))])) by
A1;
hence thesis;
end;
theorem ::
POSET_2:29
for f1,f2 be
Function of X, Y holds (E1,E2)
is_well_founded_with_minimal_set D & (for x be
Element of X holds (x
in D implies (f1
. x)
= (I
. x)) & ( not x
in D implies (f1
. x)
= (J
.
[x, (f1
. (E1
. x)), (f1
. (E2
. x))]))) & (for x be
Element of X holds (x
in D implies (f2
. x)
= (I
. x)) & ( not x
in D implies (f2
. x)
= (J
.
[x, (f2
. (E1
. x)), (f2
. (E2
. x))]))) implies f1
= f2
proof
let f1,f2 be
Function of X, Y;
assume
A0: (E1,E2)
is_well_founded_with_minimal_set D & (for x be
Element of X holds (x
in D implies (f1
. x)
= (I
. x)) & ( not x
in D implies (f1
. x)
= (J
.
[x, (f1
. (E1
. x)), (f1
. (E2
. x))]))) & (for x be
Element of X holds (x
in D implies (f2
. x)
= (I
. x)) & ( not x
in D implies (f2
. x)
= (J
.
[x, (f2
. (E1
. x)), (f2
. (E2
. x))])));
then
consider l be
Function of X,
NAT such that
A1: for x be
Element of X holds ((l
. x)
<=
0 implies x
in D) & ( not x
in D implies (l
. (E1
. x))
< (l
. x) & (l
. (E2
. x))
< (l
. x));
defpred
P[
Nat] means for x be
Element of X st (l
. x)
<= $1 holds (f1
. x)
= (f2
. x);
A2:
P[
0 ]
proof
let x be
Element of X;
assume
b1: (l
. x)
<=
0 ;
then (f1
. x)
= (I
. x) by
A0,
A1
.= (f2
. x) by
A0,
b1,
A1;
hence thesis;
end;
A3: for k st
P[k] holds
P[(k
+ 1)]
proof
let k;
assume
B0:
P[k];
let x be
Element of X;
assume
B1: (l
. x)
<= (k
+ 1);
per cases ;
suppose
C0: x
in D;
(f1
. x)
= (I
. x) by
A0,
C0
.= (f2
. x) by
A0,
C0;
hence thesis;
end;
suppose
C0: not x
in D;
set x1 = (E1
. x), x2 = (E2
. x);
reconsider x as
Element of X;
((l
. x1)
+ 1)
<= (l
. x) & ((l
. x2)
+ 1)
<= (l
. x) by
NAT_1: 13,
A1,
C0;
then ((l
. x1)
+ 1)
<= (k
+ 1) & ((l
. x2)
+ 1)
<= (k
+ 1) by
B1,
XXREAL_0: 2;
then
C2: (f1
. x1)
= (f2
. x1) & (f1
. x2)
= (f2
. x2) by
B0,
XREAL_1: 8;
(f1
. x)
= (J
.
[x, (f1
. x1), (f1
. x2)]) by
A0,
C0
.= (f2
. x) by
C2,
A0,
C0;
hence thesis;
end;
end;
A4: for k be
Nat holds
P[k] from
NAT_1:sch 2(
A2,
A3);
for x be
Element of X holds (f1
. x)
= (f2
. x)
proof
let x be
Element of X;
reconsider k = (l
. x) as
Nat;
(l
. x)
<= k;
hence thesis by
A4;
end;
hence thesis;
end;