:: Retracts and Inheritance
:: by Grzegorz Bancerek
::
:: Received September 7, 1999
:: Copyright (c) 1999-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies RELAT_1, TARSKI, XBOOLE_0, ORDERS_2, YELLOW_0, FUNCT_1, STRUCT_0,
XXREAL_0, SUBSET_1, CAT_1, RELAT_2, WAYBEL_0, SEQM_3, FUNCOP_1, ORDINAL2,
BINOP_1, GROUP_6, EQREL_1, FUNCT_3, BORSUK_1, WAYBEL_1, WELLORD1,
REWRITE1, YELLOW_1, WAYBEL_3, NEWTON, CARD_3, PBOOLE, LATTICE3, FUNCT_4,
RLVECT_2, ZFMISC_1, LATTICES, PRE_TOPC, RCOMP_1, WAYBEL18, CARD_1,
YELLOW_9, T_0TOPSP, TOPS_2, YELLOW16, FUNCT_2;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1,
PBOOLE, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_3, ORDINAL1, NUMBERS, FUNCT_7,
FUNCOP_1, STRUCT_0, CARD_3, PRALG_1, FUNCT_4, WELLORD1, ORDERS_2,
LATTICE3, PRE_TOPC, TOPS_2, T_0TOPSP, BORSUK_1, QUANTAL1, YELLOW_0,
WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, YELLOW_9, WAYBEL_3, WAYBEL18;
constructors TOLER_1, FUNCT_7, TOPS_2, BORSUK_1, T_0TOPSP, MONOID_0, QUANTAL1,
ORDERS_3, YELLOW_9, WAYBEL18, WAYBEL20, FUNCT_4;
registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCT_2, FUNCOP_1, STRUCT_0,
PRE_TOPC, TOPS_1, BORSUK_1, LATTICE3, YELLOW_0, MONOID_0, BORSUK_2,
WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, WAYBEL_3, WAYBEL10, WAYBEL17,
WAYBEL18, RELAT_1;
requirements SUBSET, BOOLE, NUMERALS;
definitions TARSKI, RELAT_1, LATTICE3, YELLOW_0, BORSUK_1, WAYBEL_0, YELLOW_1,
YELLOW_2, WAYBEL_1, WAYBEL_3, T_0TOPSP, WAYBEL25, XBOOLE_0;
equalities ORDINAL1, YELLOW_1, YELLOW_2, WAYBEL_1, STRUCT_0;
expansions TARSKI, LATTICE3, YELLOW_0, BORSUK_1, WAYBEL_0, YELLOW_2, WAYBEL_1,
T_0TOPSP;
theorems YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, PRE_TOPC, BORSUK_1,
ORDERS_2, YELLOW12, RELAT_1, FUNCT_2, FUNCT_1, ENUMSET1, WAYBEL_3,
FUNCOP_1, CARD_3, TARSKI, ZFMISC_1, WELLORD1, QUANTAL1, FUNCT_4,
YELLOW_9, WAYBEL20, FUNCT_7, TOPS_2, FUNCT_3, WAYBEL10, WAYBEL15,
YELLOW_6, PRALG_1, WAYBEL18, WAYBEL13, WAYBEL21, XBOOLE_0, XBOOLE_1,
PARTFUN1, CARD_1;
schemes PBOOLE;
begin :: Poset retracts
::$CT
theorem
for X being set, L being non empty RelStr, S being non empty SubRelStr
of L for f,g being Function of X, the carrier of S for f9,g9 being Function of
X, the carrier of L st f9 = f & g9 = g & f <= g holds f9 <= g9
proof
let X be set, L be non empty RelStr, S be non empty SubRelStr of L;
let f,g be Function of X, the carrier of S;
let f9,g9 be Function of X, the carrier of L such that
A1: f9 = f and
A2: g9 = g and
A3: f <= g;
let x be set;
assume
A4: x in X;
then reconsider a = f.x, b = g.x as Element of S by FUNCT_2:5;
reconsider a9 = a, b9 = b as Element of L by YELLOW_0:58;
take a9, b9;
thus a9 = f9.x & b9 = g9.x by A1,A2;
ex a,b being Element of S st a = f.x & b = g.x & a <= b by A3,A4;
hence thesis by YELLOW_0:59;
end;
theorem
for X being set, L being non empty RelStr for S being full non empty
SubRelStr of L for f,g being Function of X, the carrier of S for f9,g9 being
Function of X, the carrier of L st f9 = f & g9 = g & f9 <= g9 holds f <= g
proof
let X be set, L be non empty RelStr;
let S be full non empty SubRelStr of L;
let f,g be Function of X, the carrier of S;
let f9,g9 be Function of X, the carrier of L such that
A1: f9 = f and
A2: g9 = g and
A3: f9 <= g9;
let x be set;
assume
A4: x in X;
then reconsider a = f.x, b = g.x as Element of S by FUNCT_2:5;
take a, b;
thus a = f.x & b = g.x;
ex a9,b9 being Element of L st a9 = a & b9 = b & a9 <= b9 by A1,A2,A3,A4;
hence thesis by YELLOW_0:60;
end;
registration
let S be non empty RelStr;
let T be non empty reflexive antisymmetric RelStr;
cluster directed-sups-preserving monotone for Function of S,T;
existence
proof
set x = the Element of T;
take f = S --> x;
thus f is directed-sups-preserving
proof
let X be Subset of S;
assume
A1: X is non empty directed;
A2: f.:X = {x}
proof
set a = the Element of X;
thus f.:X c= {x} by FUNCOP_1:81;
A3: dom f = the carrier of S by FUNCOP_1:13;
A4: a in X by A1;
then f.a = x by FUNCOP_1:7;
then x in f.:X by A4,A3,FUNCT_1:def 6;
hence thesis by ZFMISC_1:31;
end;
assume ex_sup_of X,S;
thus ex_sup_of f.:X, T by A2,YELLOW_0:38;
thus sup (f.:X) = x by A2,YELLOW_0:39
.= f.sup X by FUNCOP_1:7;
end;
let a,b be Element of S;
A5: x <= x;
f.a = x by FUNCOP_1:7;
hence thesis by A5,FUNCOP_1:7;
end;
end;
theorem
for f,g being Function st f is idempotent & rng g c= rng f & rng g c=
dom f holds f*g = g
proof
let f,g be Function;
assume f is idempotent;
then
A1: f*f = f by QUANTAL1:def 9;
assume
A2: rng g c= rng f;
A3: now
let x be object;
assume
A4: x in dom g;
then g.x in rng g by FUNCT_1:def 3;
then
A5: ex a being object st a in dom f & g.x = f.a by A2,FUNCT_1:def 3;
(f*g).x = f.(g.x) by A4,FUNCT_1:13;
hence (f*g).x = g.x by A1,A5,FUNCT_1:13;
end;
assume rng g c= dom f;
then dom (f*g) = dom g by RELAT_1:27;
hence thesis by A3,FUNCT_1:2;
end;
registration
let S be 1-sorted;
cluster idempotent for Function of S,S;
existence
proof
take f = id S;
f*f = f by FUNCT_2:17;
hence thesis by QUANTAL1:def 9;
end;
end;
theorem Th4:
for L being up-complete non empty Poset for S being
directed-sups-inheriting full non empty SubRelStr of L holds S is up-complete
proof
let L be up-complete non empty Poset;
let S be directed-sups-inheriting full non empty SubRelStr of L;
now
let X be non empty directed Subset of S;
reconsider Y = X as non empty directed Subset of L by YELLOW_2:7;
ex_sup_of Y,L by WAYBEL_0:75;
hence ex_sup_of X,S by WAYBEL_0:7;
end;
hence thesis by WAYBEL_0:75;
end;
theorem Th5:
for L being up-complete non empty Poset for f being Function of
L, L st f is idempotent directed-sups-preserving holds Image f is
directed-sups-inheriting
proof
let L be up-complete non empty Poset;
let f be Function of L, L;
set S = subrelstr(rng f);
set a = the Element of L;
reconsider S9 = S as non empty full SubRelStr of L;
assume
A1: f is idempotent directed-sups-preserving;
S is directed-sups-inheriting
proof
let X be directed Subset of S;
X c= the carrier of S;
then
A2: X c= rng f by YELLOW_0:def 15;
assume X <> {};
then X is non empty directed Subset of S9;
then reconsider X9= X as non empty directed Subset of L by YELLOW_2:7;
assume
A3: ex_sup_of X,L;
f preserves_sup_of X9 by A1;
then sup(f.:X9) = f.sup X9 by A3;
then sup X9 = f.sup X9 by A1,A2,YELLOW_2:20;
then "\/"(X, L) in rng f by FUNCT_2:4;
hence thesis by YELLOW_0:def 15;
end;
hence thesis;
end;
theorem Th6:
for T being non empty RelStr, S being non empty SubRelStr of T
for f being Function of T,S holds f*incl(S,T) = id S implies f is idempotent
Function of T, T
proof
let T be non empty RelStr, S be non empty SubRelStr of T;
let f be Function of T,S;
assume
A1: f*incl(S, T) = id S;
A2: the carrier of S c= the carrier of T by YELLOW_0:def 13;
then incl(S, T) = id the carrier of S by YELLOW_9:def 1;
then incl(S, T)*f = f by FUNCT_2:17;
then
A3: f*f = (id the carrier of S)*f by A1,RELAT_1:36
.= f by FUNCT_2:17;
A4: dom f = the carrier of T by FUNCT_2:def 1;
f is onto by A1,FUNCT_2:23;
then rng f = the carrier of S by FUNCT_2:def 3;
hence thesis by A2,A3,A4,FUNCT_2:2,QUANTAL1:def 9;
end;
definition
let S,T be non empty Poset;
let f be Function;
pred f is_a_retraction_of T,S means
f is directed-sups-preserving
Function of T,S & f|the carrier of S = id S & S is directed-sups-inheriting
full SubRelStr of T;
pred f is_an_UPS_retraction_of T,S means
f is
directed-sups-preserving Function of T,S & ex g being directed-sups-preserving
Function of S,T st f*g = id S;
end;
definition
let S,T be non empty Poset;
pred S is_a_retract_of T means
ex f being Function of T,S st f is_a_retraction_of T,S;
pred S is_an_UPS_retract_of T means
ex f being Function of T,S st f is_an_UPS_retraction_of T,S;
end;
theorem Th7:
for S,T being non empty Poset, f being Function st f
is_a_retraction_of T,S holds f*incl(S,T) = id S
proof
let S,T be non empty Poset, f be Function such that
f is directed-sups-preserving Function of T,S and
A1: f|the carrier of S = id S and
A2: S is directed-sups-inheriting full SubRelStr of T;
the carrier of S c= the carrier of T by A2,YELLOW_0:def 13;
hence f*incl(S, T) = f*id the carrier of S by YELLOW_9:def 1
.= id S by A1,RELAT_1:65;
end;
theorem Th8:
for S being non empty Poset, T being up-complete non empty
Poset for f being Function st f is_a_retraction_of T,S holds f
is_an_UPS_retraction_of T,S
proof
let S be non empty Poset;
let T be up-complete non empty Poset, f be Function;
assume
A1: f is_a_retraction_of T,S;
hence f is directed-sups-preserving Function of T,S;
S is directed-sups-inheriting full SubRelStr of T by A1;
then reconsider
g = incl(S,T) as directed-sups-preserving Function of S,T by WAYBEL21:10;
take g;
thus thesis by A1,Th7;
end;
theorem Th9:
for S,T being non empty Poset, f being Function st f
is_a_retraction_of T,S holds rng f = the carrier of S
proof
let S,T be non empty Poset, f be Function;
assume
A1: f is_a_retraction_of T,S;
then reconsider f as Function of T,S;
f*incl(S,T) = id S by A1,Th7;
then f is onto by FUNCT_2:23;
hence thesis by FUNCT_2:def 3;
end;
theorem Th10:
for S,T being non empty Poset, f being Function st f
is_an_UPS_retraction_of T,S holds rng f = the carrier of S
proof
let S,T be non empty Poset, f be Function;
assume that
A1: f is directed-sups-preserving Function of T,S and
A2: ex g being directed-sups-preserving Function of S,T st f*g = id S;
reconsider f as Function of T,S by A1;
f is onto by A2,FUNCT_2:23;
hence thesis by FUNCT_2:def 3;
end;
theorem Th11:
for S,T being non empty Poset, f being Function st f
is_a_retraction_of T,S holds f is idempotent Function of T,T
proof
let S,T be non empty Poset, f be Function;
assume
A1: f is_a_retraction_of T,S;
then
A2: f is Function of T,S;
A3: S is SubRelStr of T by A1;
f*incl(S,T) = id S by A1,Th7;
hence thesis by A2,A3,Th6;
end;
theorem Th12:
for T,S being non empty Poset, f being Function of T,T st f
is_a_retraction_of T,S holds Image f = the RelStr of S
proof
let T,S be non empty Poset, f be Function of T,T;
A1: the carrier of Image f = rng f by YELLOW_0:def 15;
assume
A2: f is_a_retraction_of T,S;
thus thesis by A2,A1,Th9,YELLOW_0:57;
end;
theorem Th13:
for T being up-complete non empty Poset for S being non empty
Poset, f being Function of T,T st f is_a_retraction_of T,S holds f is
directed-sups-preserving projection
proof
let T be up-complete non empty Poset;
let S be non empty Poset, f be Function of T,T;
assume
A1: f is_a_retraction_of T,S;
then reconsider g = f as directed-sups-preserving Function of T,S;
f is idempotent by A1,Th11;
then
A2: f = f*f by QUANTAL1:def 9
.= (f|rng f)*f by FUNCT_4:2
.= (f|the carrier of S)*f by A1,Th8,Th10
.= (id S)*f by A1
.= (id the carrier of S)*g;
A3: S is full directed-sups-inheriting non empty SubRelStr of T by A1;
then
A4: incl(S,T) is directed-sups-preserving by WAYBEL21:10;
the carrier of S c= the carrier of T by A3,YELLOW_0:def 13;
then
A5: incl(S,T) = id the carrier of S by YELLOW_9:def 1;
hence f is directed-sups-preserving by A2,A4,WAYBEL20:28;
f is directed-sups-preserving idempotent Function of T,T by A1,A2,A4,A5,Th11,
WAYBEL20:28;
hence thesis;
end;
theorem Th14:
for S,T being non empty reflexive transitive RelStr for f being
Function of S,T holds f is isomorphic iff f is monotone & ex g being monotone
Function of T,S st f*g = id T & g*f = id S
proof
let S,T be non empty reflexive transitive RelStr, f be Function of S,T;
hereby
assume
A1: f is isomorphic;
hence f is monotone;
consider g being Function of T,S such that
A2: g = f qua Function" and
A3: g is monotone by A1,WAYBEL_0:def 38;
reconsider g as monotone Function of T,S by A3;
take g;
rng f = the carrier of T by A1,WAYBEL_0:66;
hence f*g = id T & g*f = id S by A1,A2,FUNCT_2:29;
end;
assume
A4: f is monotone;
given g being monotone Function of T,S such that
A5: f*g = id T and
A6: g*f = id S;
A7: f is one-to-one by A6,FUNCT_2:23;
f is onto by A5,FUNCT_2:23;
then rng f = the carrier of T by FUNCT_2:def 3;
then g = f qua Function" by A6,A7,FUNCT_2:30;
hence thesis by A4,A7,WAYBEL_0:def 38;
end;
theorem Th15:
for S,T being non empty Poset holds S,T are_isomorphic iff ex f
being monotone Function of S,T, g being monotone Function of T,S st f*g = id T
& g*f = id S
proof
let S,T be non empty Poset;
hereby
assume S,T are_isomorphic;
then consider f being Function of S,T such that
A1: f is isomorphic;
reconsider f as monotone Function of S,T by A1;
consider g being Function of T,S such that
A2: g = f qua Function" and
A3: g is monotone by A1,WAYBEL_0:def 38;
take f;
reconsider g as monotone Function of T,S by A3;
take g;
rng f = the carrier of T by A1,WAYBEL_0:66;
hence f*g = id T & g*f = id S by A1,A2,FUNCT_2:29;
end;
given f being monotone Function of S,T, g being monotone Function of T,S
such that
A4: f*g = id T and
A5: g*f = id S;
take f;
A6: f is one-to-one by A5,FUNCT_2:23;
f is onto by A4,FUNCT_2:23;
then rng f = the carrier of T by FUNCT_2:def 3;
then g = f qua Function" by A5,A6,FUNCT_2:30;
hence thesis by A6,WAYBEL_0:def 38;
end;
theorem
for S,T being up-complete non empty Poset st S,T are_isomorphic
holds S is_an_UPS_retract_of T & T is_an_UPS_retract_of S
proof
let S,T be up-complete non empty Poset;
assume S,T are_isomorphic;
then consider
f be monotone Function of S,T, g be monotone Function of T,S such
that
A1: f*g = id T and
A2: g*f = id S by Th15;
g is isomorphic by A1,A2,Th14;
then
A3: g is sups-preserving by WAYBEL13:20;
f is isomorphic by A1,A2,Th14;
then
A4: f is sups-preserving by WAYBEL13:20;
then
A5: f is_an_UPS_retraction_of S,T by A1,A3;
g is_an_UPS_retraction_of T,S by A2,A4,A3;
hence thesis by A5;
end;
theorem Th17:
for T,S being non empty Poset for f being monotone Function of T
,S, g being monotone Function of S,T st f*g = id S ex h being projection
Function of T,T st h = g*f & h|the carrier of Image h = id Image h & S, Image h
are_isomorphic
proof
let T,S be non empty Poset;
let f be monotone Function of T,S, g be monotone Function of S,T such that
A1: f*g = id S;
set h = g*f;
h*h = h*g*f by RELAT_1:36
.= g*(id S)*f by A1,RELAT_1:36
.= h by FUNCT_2:17;
then h is idempotent monotone Function of T,T by QUANTAL1:def 9,YELLOW_2:12;
then reconsider h as projection Function of T,T by WAYBEL_1:def 13;
A2: dom g = the carrier of S by FUNCT_2:def 1;
f is onto by A1,FUNCT_2:23;
then
A3: rng f = the carrier of S by FUNCT_2:def 3;
then reconsider gg = corestr g as Function of S, Image h by A2,RELAT_1:28;
A4: gg = g by WAYBEL_1:30;
A5: now
let x,y be Element of S;
x <= y implies g.x <= g.y & gg.x in the carrier of Image h by
WAYBEL_1:def 2;
hence x <= y implies gg.x <= gg.y by A4,YELLOW_0:60;
(id S).x = x;
then
A6: x = f.(g.x) by A1,FUNCT_2:15;
(id S).y = y;
then
A7: y = f.(g.y) by A1,FUNCT_2:15;
assume gg.x <= gg.y;
then g.x <= g.y by A4,YELLOW_0:59;
hence x <= y by A6,A7,WAYBEL_1:def 2;
end;
rng h = rng g by A3,A2,RELAT_1:28;
then
A8: rng gg = the carrier of Image h by A4,YELLOW_0:def 15;
take h;
thus h = g*f;
thus h|the carrier of Image h = h*(inclusion h) by RELAT_1:65
.= (corestr h)*(inclusion h) by WAYBEL_1:30
.= id Image h by WAYBEL_1:33;
take gg;
gg is one-to-one by A1,A4,FUNCT_2:23;
hence thesis by A8,A5,WAYBEL_0:66;
end;
theorem Th18:
for T being up-complete non empty Poset, S being non empty
Poset for f being Function st f is_an_UPS_retraction_of T,S ex h being
directed-sups-preserving projection Function of T,T st h is_a_retraction_of T,
Image h & S, Image h are_isomorphic
proof
let T be up-complete non empty Poset;
let S be non empty Poset, f be Function such that
A1: f is directed-sups-preserving Function of T,S;
given g being directed-sups-preserving Function of S,T such that
A2: f*g = id S;
reconsider f as directed-sups-preserving Function of T,S by A1;
consider h being projection Function of T,T such that
A3: h = g*f and
A4: h|the carrier of Image h = id Image h and
A5: S, Image h are_isomorphic by A2,Th17;
reconsider h as directed-sups-preserving projection Function of T,T by A3,
WAYBEL20:28;
take h;
reconsider R = Image h as non empty Poset;
h = corestr h by WAYBEL_1:30;
then
A6: h is directed-sups-preserving Function of T, R by WAYBEL20:22;
R is directed-sups-inheriting full SubRelStr of T by Th5;
hence h is_a_retraction_of T, Image h by A4,A6;
thus thesis by A5;
end;
theorem Th19:
for L being up-complete non empty Poset for S being non empty
Poset st S is_a_retract_of L holds S is up-complete
proof
let L be up-complete non empty Poset;
let S be non empty Poset;
given f being Function of L,S such that
A1: f is_a_retraction_of L,S;
S is full directed-sups-inheriting non empty SubRelStr of L by A1;
hence thesis by Th4;
end;
theorem Th20:
for L being complete non empty Poset for S being non empty
Poset st S is_a_retract_of L holds S is complete
proof
let L be complete non empty Poset;
let S be non empty Poset;
given f being Function of L, S such that
A1: f is_a_retraction_of L,S;
reconsider f as directed-sups-preserving projection Function of L,L by A1
,Th11,Th13;
A2: Image f is complete by YELLOW_2:35;
the RelStr of S = Image f by A1,Th12;
hence thesis by A2,YELLOW_0:3;
end;
theorem Th21:
for L being continuous complete LATTICE for S being non empty
Poset st S is_a_retract_of L holds S is continuous
proof
let L be continuous complete LATTICE;
let S be non empty Poset;
given f being Function of L,S such that
A1: f is_a_retraction_of L,S;
reconsider g = f as directed-sups-preserving projection Function of L,L by A1
,Th11,Th13;
A2: Image g is continuous LATTICE by WAYBEL15:15;
Image g = the RelStr of S by A1,Th12;
hence thesis by A2,YELLOW12:15;
end;
theorem
for L being up-complete non empty Poset for S being non empty Poset
st S is_an_UPS_retract_of L holds S is up-complete
proof
let L be up-complete non empty Poset;
let S be non empty Poset;
given f being Function of L,S such that
A1: f is_an_UPS_retraction_of L,S;
consider h being directed-sups-preserving projection Function of L,L such
that
A2: h is_a_retraction_of L, Image h and
A3: S, Image h are_isomorphic by A1,Th18;
Image h is_a_retract_of L by A2;
then Image h is up-complete by Th19;
hence thesis by A3,WAYBEL13:30,WAYBEL_1:6;
end;
theorem
for L being complete non empty Poset for S being non empty Poset st
S is_an_UPS_retract_of L holds S is complete
proof
let L be complete non empty Poset, S be non empty Poset;
given f being Function of L, S such that
A1: f is_an_UPS_retraction_of L,S;
consider h being directed-sups-preserving projection Function of L,L such
that
A2: h is_a_retraction_of L, Image h and
A3: S, Image h are_isomorphic by A1,Th18;
Image h is_a_retract_of L by A2;
then Image h is complete by Th20;
hence thesis by A3,WAYBEL20:18,WAYBEL_1:6;
end;
theorem
for L being continuous complete LATTICE for S being non empty Poset st
S is_an_UPS_retract_of L holds S is continuous
proof
let L be continuous complete LATTICE;
let S be non empty Poset;
given f being Function of L,S such that
A1: f is_an_UPS_retraction_of L,S;
consider h being directed-sups-preserving projection Function of L,L such
that
A2: h is_a_retraction_of L, Image h and
A3: S, Image h are_isomorphic by A1,Th18;
Image h is_a_retract_of L by A2;
then Image h is continuous by Th21;
hence thesis by A3,WAYBEL15:9,WAYBEL_1:6;
end;
theorem Th25:
for L being RelStr for S being full SubRelStr of L for R being
SubRelStr of S holds R is full iff R is full SubRelStr of L
proof
let L be RelStr, S be full SubRelStr of L, R be SubRelStr of S;
reconsider R9 = R as SubRelStr of L by YELLOW_6:7;
A1: the carrier of R c= the carrier of S by YELLOW_0:def 13;
hereby
assume R is full;
then the InternalRel of R = (the InternalRel of S)|_2 the carrier of R
.= ((the InternalRel of L)|_2 the carrier of S)|_2 the carrier of R by
YELLOW_0:def 14
.= (the InternalRel of L)|_2 the carrier of R9 by A1,WELLORD1:22;
hence R is full SubRelStr of L by YELLOW_0:def 14;
end;
assume
A2: R is full SubRelStr of L;
((the InternalRel of L)|_2 the carrier of S)|_2 the carrier of R = (the
InternalRel of L)|_2 the carrier of R by A1,WELLORD1:22
.= the InternalRel of R by A2,YELLOW_0:def 14;
hence the InternalRel of R = (the InternalRel of S)|_2 the carrier of R by
YELLOW_0:def 14;
end;
theorem
for L being non empty transitive RelStr for S being
directed-sups-inheriting non empty full SubRelStr of L for R being
directed-sups-inheriting non empty SubRelStr of S holds R is
directed-sups-inheriting SubRelStr of L
proof
let L be non empty transitive RelStr;
let S be directed-sups-inheriting non empty full SubRelStr of L;
let R be directed-sups-inheriting non empty SubRelStr of S;
reconsider T = R as SubRelStr of L by YELLOW_6:7;
T is directed-sups-inheriting
proof
let X be directed Subset of T;
reconsider Y = X as directed Subset of S by YELLOW_2:7;
assume
A1: X <> {};
assume
A2: ex_sup_of X,L;
then
A3: ex_sup_of Y, S by A1,WAYBEL_0:7;
sup Y = "\/"(X,L) by A1,A2,WAYBEL_0:7;
hence thesis by A1,A3,WAYBEL_0:def 4;
end;
hence thesis;
end;
theorem
for L being up-complete non empty Poset for S1,S2 being
directed-sups-inheriting full non empty SubRelStr of L st S1 is SubRelStr of S2
holds S1 is directed-sups-inheriting full SubRelStr of S2
proof
let L be up-complete non empty Poset;
let S1,S2 be directed-sups-inheriting full non empty SubRelStr of L;
assume S1 is SubRelStr of S2;
then reconsider S = S1 as SubRelStr of S2;
S is directed-sups-inheriting
proof
let X be directed Subset of S;
assume X <> {};
then reconsider Y1 = X as non empty directed Subset of S1;
reconsider Y2 = Y1 as non empty directed Subset of S2 by YELLOW_2:7;
reconsider Y = Y1 as non empty directed Subset of L by YELLOW_2:7;
A1: ex_sup_of Y, L by WAYBEL_0:75;
then
A2: sup Y = sup Y1 by WAYBEL_0:7;
sup Y2 = sup Y by A1,WAYBEL_0:7;
hence thesis by A2;
end;
hence thesis by Th25;
end;
begin :: Products
definition
let R be Relation;
attr R is Poset-yielding means
:Def5:
for x being set st x in rng R holds x is Poset;
end;
registration
cluster Poset-yielding -> RelStr-yielding reflexive-yielding for Relation;
coherence
proof
let R be Relation;
assume
A1: for x being set st x in rng R holds x is Poset;
hence for x being set st x in rng R holds x is RelStr;
thus for S being RelStr st S in rng R holds S is reflexive by A1;
end;
end;
definition
let X be non empty set;
let L be non empty RelStr;
let i be Element of X;
let Y be Subset of L|^X;
redefine func pi(Y,i) -> Subset of L;
coherence
proof
reconsider Y9 = Y as Subset of product (X --> L);
pi(Y9,i) is Subset of (X --> L).i;
hence thesis by FUNCOP_1:7;
end;
end;
registration
let X be set;
let S be Poset;
cluster X --> S -> Poset-yielding;
coherence
proof
let x be set;
assume x in rng (X --> S);
hence thesis by TARSKI:def 1;
end;
end;
registration
let I be set;
cluster Poset-yielding non-Empty for ManySortedSet of I;
existence
proof
set P = the non empty Poset;
take I --> P;
thus thesis;
end;
end;
registration
let I be non empty set;
let J be Poset-yielding non-Empty ManySortedSet of I;
cluster product J -> transitive antisymmetric;
coherence
proof
A1: now
let i be Element of I;
dom J = I by PARTFUN1:def 2;
then J.i in rng J by FUNCT_1:def 3;
hence J.i is Poset by Def5;
end;
then for i being Element of I holds J.i is transitive;
hence product J is transitive by WAYBEL_3:29;
for i being Element of I holds J.i is antisymmetric by A1;
hence thesis by WAYBEL_3:30;
end;
end;
definition
let I be non empty set;
let J be Poset-yielding non-Empty ManySortedSet of I;
let i be Element of I;
redefine func J.i -> non empty Poset;
coherence
proof
dom J = I by PARTFUN1:def 2;
then J.i in rng J by FUNCT_1:def 3;
hence thesis by Def5;
end;
end;
Lm1: now
let I be non empty set;
let J be Poset-yielding non-Empty ManySortedSet of I;
let X be Subset of product J;
deffunc F(Element of I) = sup pi(X,$1);
consider f being ManySortedSet of I such that
A1: for i being Element of I holds f.i = F(i) from PBOOLE:sch 5;
A2: now
let i be Element of I;
f.i = sup pi(X,i) by A1;
hence f.i is Element of J.i;
end;
dom f = I by PARTFUN1:def 2;
then reconsider f as Element of product J by A2,WAYBEL_3:27;
assume
A3: for i being Element of I holds ex_sup_of pi(X,i), J.i;
take f;
thus for i being Element of I holds f.i = sup pi(X,i) by A1;
thus f is_>=_than X
proof
let x be Element of product J such that
A4: x in X;
now
let i be Element of I;
A5: f.i = sup pi(X,i) by A1;
A6: x.i in pi(X,i) by A4,CARD_3:def 6;
ex_sup_of pi(X,i), J.i by A3;
then f.i is_>=_than pi(X,i) by A5,YELLOW_0:30;
hence x.i <= f.i by A6;
end;
hence thesis by WAYBEL_3:28;
end;
let g be Element of product J;
assume
A7: X is_<=_than g;
now
let i be Element of I;
A8: ex_sup_of pi(X,i), J.i by A3;
A9: g.i is_>=_than pi(X,i)
proof
let a be Element of J.i;
assume a in pi(X,i);
then consider h being Function such that
A10: h in X and
A11: a = h.i by CARD_3:def 6;
reconsider h as Element of product J by A10;
h <= g by A7,A10;
hence a <= g.i by A11,WAYBEL_3:28;
end;
f.i = sup pi(X,i) by A1;
hence f.i <= g.i by A8,A9,YELLOW_0:30;
end;
hence f <= g by WAYBEL_3:28;
end;
Lm2: now
let I be non empty set;
let J be Poset-yielding non-Empty ManySortedSet of I;
let X be Subset of product J;
deffunc F(Element of I) = inf pi(X,$1);
consider f being ManySortedSet of I such that
A1: for i being Element of I holds f.i = F(i) from PBOOLE:sch 5;
A2: now
let i be Element of I;
f.i = inf pi(X,i) by A1;
hence f.i is Element of J.i;
end;
dom f = I by PARTFUN1:def 2;
then reconsider f as Element of product J by A2,WAYBEL_3:27;
assume
A3: for i being Element of I holds ex_inf_of pi(X,i), J.i;
take f;
thus for i being Element of I holds f.i = inf pi(X,i) by A1;
thus f is_<=_than X
proof
let x be Element of product J such that
A4: x in X;
now
let i be Element of I;
A5: f.i = inf pi(X,i) by A1;
A6: x.i in pi(X,i) by A4,CARD_3:def 6;
ex_inf_of pi(X,i), J.i by A3;
then f.i is_<=_than pi(X,i) by A5,YELLOW_0:31;
hence x.i >= f.i by A6;
end;
hence thesis by WAYBEL_3:28;
end;
let g be Element of product J;
assume
A7: X is_>=_than g;
now
let i be Element of I;
A8: ex_inf_of pi(X,i), J.i by A3;
A9: g.i is_<=_than pi(X,i)
proof
let a be Element of J.i;
assume a in pi(X,i);
then consider h being Function such that
A10: h in X and
A11: a = h.i by CARD_3:def 6;
reconsider h as Element of product J by A10;
h >= g by A7,A10;
hence a >= g.i by A11,WAYBEL_3:28;
end;
f.i = inf pi(X,i) by A1;
hence f.i >= g.i by A8,A9,YELLOW_0:31;
end;
hence f >= g by WAYBEL_3:28;
end;
theorem Th28:
for I being non empty set for J being Poset-yielding non-Empty
ManySortedSet of I for f being Element of product J, X being Subset of product
J holds f is_>=_than X iff for i being Element of I holds f.i is_>=_than pi(X,i
)
proof
let I be non empty set;
let J be Poset-yielding non-Empty ManySortedSet of I;
let f be Element of product J, X be Subset of product J;
hereby
assume
A1: f is_>=_than X;
let i be Element of I;
thus f.i is_>=_than pi(X, i)
proof
let x be Element of J.i;
assume x in pi(X, i);
then consider g being Function such that
A2: g in X and
A3: x = g.i by CARD_3:def 6;
reconsider g as Element of product J by A2;
g <= f by A1,A2;
hence thesis by A3,WAYBEL_3:28;
end;
end;
assume
A4: for i being Element of I holds f.i is_>=_than pi(X,i);
let g be Element of product J;
assume
A5: g in X;
now
let i be Element of I;
A6: f.i is_>=_than pi(X,i) by A4;
g.i in pi(X,i) by A5,CARD_3:def 6;
hence g.i <= f.i by A6;
end;
hence thesis by WAYBEL_3:28;
end;
theorem Th29:
for I being non empty set for J being Poset-yielding non-Empty
ManySortedSet of I for f being Element of product J, X being Subset of product
J holds f is_<=_than X iff for i being Element of I holds f.i is_<=_than pi(X,i
)
proof
let I be non empty set;
let J be Poset-yielding non-Empty ManySortedSet of I;
let f be Element of product J, X be Subset of product J;
hereby
assume
A1: f is_<=_than X;
let i be Element of I;
thus f.i is_<=_than pi(X, i)
proof
let x be Element of J.i;
assume x in pi(X, i);
then consider g being Function such that
A2: g in X and
A3: x = g.i by CARD_3:def 6;
reconsider g as Element of product J by A2;
g >= f by A1,A2;
hence thesis by A3,WAYBEL_3:28;
end;
end;
assume
A4: for i being Element of I holds f.i is_<=_than pi(X,i);
let g be Element of product J;
assume
A5: g in X;
now
let i be Element of I;
A6: f.i is_<=_than pi(X,i) by A4;
g.i in pi(X,i) by A5,CARD_3:def 6;
hence g.i >= f.i by A6;
end;
hence thesis by WAYBEL_3:28;
end;
theorem Th30:
for I being non empty set for J being Poset-yielding non-Empty
ManySortedSet of I for X being Subset of product J holds ex_sup_of X, product J
iff for i being Element of I holds ex_sup_of pi(X,i), J.i
proof
let I be non empty set;
let J be Poset-yielding non-Empty ManySortedSet of I;
let X be Subset of product J;
hereby
set f = sup X;
assume
A1: ex_sup_of X, product J;
let i be Element of I;
A2: now
let x be Element of J.i;
assume
A3: pi(X,i) is_<=_than x;
set g = f+*(i,x);
A4: dom g = dom f by FUNCT_7:30;
dom f = I by WAYBEL_3:27;
then
A5: g.i = x by FUNCT_7:31;
now
let j be Element of I;
g.j = f.j or g.j = x & j = i by A5,FUNCT_7:32;
hence g.j is Element of J.j;
end;
then reconsider g as Element of product J by A4,WAYBEL_3:27;
A6: X is_<=_than f by A1,YELLOW_0:30;
X is_<=_than g
proof
let h be Element of product J;
assume
A7: h in X;
then
A8: h.i in pi(X, i) by CARD_3:def 6;
A9: h <= f by A6,A7;
now
let j be Element of I;
g.j = f.j or g.j = x & j = i by A5,FUNCT_7:32;
hence h.j <= g.j by A3,A9,A8,WAYBEL_3:28;
end;
hence h <= g by WAYBEL_3:28;
end;
then f <= g by A1,YELLOW_0:30;
hence f.i <= x by A5,WAYBEL_3:28;
end;
f is_>=_than X by A1,YELLOW_0:30;
then f.i is_>=_than pi(X, i) by Th28;
hence ex_sup_of pi(X, i), J.i by A2,YELLOW_0:30;
end;
assume for i being Element of I holds ex_sup_of pi(X,i), J.i;
then ex f being Element of product J st ( for i being Element of I holds f.i
= sup pi(X,i))& f is_>=_than X & for g being Element of product J st X
is_<=_than g holds f <= g by Lm1;
hence thesis by YELLOW_0:30;
end;
theorem Th31:
for I being non empty set for J being Poset-yielding non-Empty
ManySortedSet of I for X being Subset of product J holds ex_inf_of X, product J
iff for i being Element of I holds ex_inf_of pi(X,i), J.i
proof
let I be non empty set;
let J be Poset-yielding non-Empty ManySortedSet of I;
let X be Subset of product J;
hereby
set f = inf X;
assume
A1: ex_inf_of X, product J;
let i be Element of I;
A2: f is_<=_than X by A1,YELLOW_0:31;
A3: now
let x be Element of J.i;
set g = f+*(i,x);
A4: dom g = dom f by FUNCT_7:30;
dom f = I by WAYBEL_3:27;
then
A5: g.i = x by FUNCT_7:31;
now
let j be Element of I;
g.j = f.j or g.j = x & j = i by A5,FUNCT_7:32;
hence g.j is Element of J.j;
end;
then reconsider g as Element of product J by A4,WAYBEL_3:27;
assume
A6: pi(X,i) is_>=_than x;
X is_>=_than g
proof
let h be Element of product J;
assume
A7: h in X;
then
A8: h.i in pi(X, i) by CARD_3:def 6;
A9: h >= f by A2,A7;
now
let j be Element of I;
g.j = f.j or g.j = x & j = i by A5,FUNCT_7:32;
hence h.j >= g.j by A6,A9,A8,WAYBEL_3:28;
end;
hence thesis by WAYBEL_3:28;
end;
then f >= g by A1,YELLOW_0:31;
hence f.i >= x by A5,WAYBEL_3:28;
end;
f.i is_<=_than pi(X, i) by A2,Th29;
hence ex_inf_of pi(X, i), J.i by A3,YELLOW_0:31;
end;
assume for i being Element of I holds ex_inf_of pi(X,i), J.i;
then ex f being Element of product J st ( for i being Element of I holds f.i
= inf pi(X,i))& f is_<=_than X & for g being Element of product J st X
is_>=_than g holds f >= g by Lm2;
hence thesis by YELLOW_0:31;
end;
theorem Th32:
for I being non empty set for J being Poset-yielding non-Empty
ManySortedSet of I for X being Subset of product J st ex_sup_of X, product J
for i being Element of I holds (sup X).i = sup pi(X,i)
proof
let I be non empty set;
let J be Poset-yielding non-Empty ManySortedSet of I;
let X be Subset of product J;
assume ex_sup_of X, product J;
then for i being Element of I holds ex_sup_of pi(X,i), J.i by Th30;
then consider f being Element of product J such that
A1: for i being Element of I holds f.i = sup pi(X,i) and
A2: f is_>=_than X and
A3: for g being Element of product J st X is_<=_than g holds f <= g by Lm1;
sup X = f by A2,A3,YELLOW_0:30;
hence thesis by A1;
end;
theorem Th33:
for I being non empty set for J being Poset-yielding non-Empty
ManySortedSet of I for X being Subset of product J st ex_inf_of X, product J
for i being Element of I holds (inf X).i = inf pi(X,i)
proof
let I be non empty set;
let J be Poset-yielding non-Empty ManySortedSet of I;
let X be Subset of product J;
assume ex_inf_of X, product J;
then for i being Element of I holds ex_inf_of pi(X,i), J.i by Th31;
then consider f being Element of product J such that
A1: for i being Element of I holds f.i = inf pi(X,i) and
A2: f is_<=_than X and
A3: for g being Element of product J st X is_>=_than g holds f >= g by Lm2;
inf X = f by A2,A3,YELLOW_0:31;
hence thesis by A1;
end;
theorem Th34:
for I being non empty set for J being RelStr-yielding non-Empty
reflexive-yielding ManySortedSet of I for X being directed Subset of product J
for i being Element of I holds pi(X,i) is directed
proof
let I be non empty set;
let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I;
let X be directed Subset of product J;
let i be Element of I;
let x,y be Element of J.i;
assume x in pi(X,i);
then consider f being Function such that
A1: f in X and
A2: x = f.i by CARD_3:def 6;
assume y in pi(X,i);
then consider g being Function such that
A3: g in X and
A4: y = g.i by CARD_3:def 6;
reconsider f,g as Element of product J by A1,A3;
consider h being Element of product J such that
A5: h in X and
A6: f <= h and
A7: g <= h by A1,A3,WAYBEL_0:def 1;
take h.i;
thus h.i in pi(X,i) by A5,CARD_3:def 6;
thus thesis by A2,A4,A6,A7,WAYBEL_3:28;
end;
theorem Th35:
for I being non empty set for J,K being RelStr-yielding
non-Empty ManySortedSet of I st for i being Element of I holds K.i is SubRelStr
of J.i holds product K is SubRelStr of product J
proof
let I be non empty set;
let J,K be RelStr-yielding non-Empty ManySortedSet of I such that
A1: for i being Element of I holds K.i is SubRelStr of J.i;
A2: now
let i be object;
assume i in I;
then reconsider j = i as Element of I;
A3: ex R being 1-sorted st R = J.j & (Carrier J).j = the carrier of R by
PRALG_1:def 13;
A4: ex R being 1-sorted st R = K.j & (Carrier K).j = the carrier of R by
PRALG_1:def 13;
K.j is SubRelStr of J.j by A1;
hence (Carrier K).i c= (Carrier J).i by A3,A4,YELLOW_0:def 13;
end;
A5: dom Carrier K = I by PARTFUN1:def 2;
A6: dom Carrier J = I by PARTFUN1:def 2;
A7: the carrier of product J = product Carrier J by YELLOW_1:def 4;
the carrier of product K = product Carrier K by YELLOW_1:def 4;
hence
A8: the carrier of product K c= the carrier of product J by A7,A6,A5,A2,
CARD_3:27;
let x,y be object;
assume
A9: [x,y] in the InternalRel of product K;
reconsider x,y as Element of product K by A9,ZFMISC_1:87;
reconsider f = x, g = y as Element of product J by A8;
A10: x <= y by A9,ORDERS_2:def 5;
now
let i be Element of I;
A11: x.i <= y.i by A10,WAYBEL_3:28;
K.i is SubRelStr of J.i by A1;
hence f.i <= g.i by A11,YELLOW_0:59;
end;
then f <= g by WAYBEL_3:28;
hence thesis by ORDERS_2:def 5;
end;
theorem Th36:
for I being non empty set for J,K being RelStr-yielding
non-Empty ManySortedSet of I st for i being Element of I holds K.i is full
SubRelStr of J.i holds product K is full SubRelStr of product J
proof
let I be non empty set;
let J,K be RelStr-yielding non-Empty ManySortedSet of I;
assume
A1: for i being Element of I holds K.i is full SubRelStr of J.i;
then for i being Element of I holds K.i is SubRelStr of J.i;
then reconsider S = product K as non empty SubRelStr of product J by Th35;
A2: (the InternalRel of product J)|_2 the carrier of S = (the InternalRel of
product J)/\[:the carrier of S,the carrier of S:] by WELLORD1:def 6;
S is full
proof
the InternalRel of S c= the InternalRel of product J by YELLOW_0:def 13;
hence
the InternalRel of S c= (the InternalRel of product J)|_2 the carrier
of S by A2,XBOOLE_1:19;
let x,y be object;
assume
A3: [x,y] in (the InternalRel of product J)|_2 the carrier of S;
then
A4: [x,y] in the InternalRel of product J by A2,XBOOLE_0:def 4;
[x,y] in [:the carrier of S, the carrier of S:] by A2,A3,XBOOLE_0:def 4;
then reconsider x, y as Element of S by ZFMISC_1:87;
reconsider a = x, b = y as Element of product J by YELLOW_0:58;
reconsider x, y as Element of product K;
A5: a <= b by A4,ORDERS_2:def 5;
now
let i be Element of I;
A6: K.i is full SubRelStr of J.i by A1;
a.i <= b.i by A5,WAYBEL_3:28;
hence x.i <= y.i by A6,YELLOW_0:60;
end;
then x <= y by WAYBEL_3:28;
hence thesis by ORDERS_2:def 5;
end;
hence thesis;
end;
theorem
for L being non empty RelStr, S being non empty SubRelStr of L, X
being set holds S|^X is SubRelStr of L|^X
proof
let L be non empty RelStr, S be non empty SubRelStr of L, X be set;
per cases;
suppose
A1: X = {};
then
A2: L|^X = RelStr (#{{}}, id { {}}#) by YELLOW_1:27;
S|^X = RelStr (#{{}}, id {{}}#) by A1,YELLOW_1:27;
hence thesis by A2,YELLOW_6:6;
end;
suppose
X <> {};
then reconsider X as non empty set;
now
let i be Element of X;
(X --> L).i = L by FUNCOP_1:7;
hence (X --> S).i is SubRelStr of (X --> L).i by FUNCOP_1:7;
end;
hence thesis by Th35;
end;
end;
theorem Th38:
for L being non empty RelStr, S be full non empty SubRelStr of L
, X be set holds S|^X is full SubRelStr of L|^X
proof
let L be non empty RelStr, S be full non empty SubRelStr of L, X be set;
per cases;
suppose
A1: X = {};
then
A2: L|^X = RelStr (#{{}},id {{}}#) by YELLOW_1:27;
S|^X = RelStr (#{{}}, id {{}}#) by A1,YELLOW_1:27;
hence thesis by A2,YELLOW_6:6;
end;
suppose
X <> {};
then reconsider X as non empty set;
now
let i be Element of X;
(X --> L).i = L by FUNCOP_1:7;
hence (X --> S).i is full SubRelStr of (X --> L).i by FUNCOP_1:7;
end;
hence thesis by Th36;
end;
end;
begin :: Inheritance
definition
let S,T be non empty RelStr, X be set;
pred S inherits_sup_of X,T means
ex_sup_of X,T implies "\/"(X, T) in the carrier of S;
pred S inherits_inf_of X,T means
ex_inf_of X,T implies "/\"(X, T) in the carrier of S;
end;
theorem
for T being non empty transitive RelStr for S being full non
empty SubRelStr of T for X being Subset of S holds S inherits_sup_of X,T iff (
ex_sup_of X,T implies ex_sup_of X, S & sup X = "\/"(X, T))
by YELLOW_0:64;
theorem
for T being non empty transitive RelStr for S being full non empty
SubRelStr of T for X being Subset of S holds S inherits_inf_of X,T iff (
ex_inf_of X,T implies ex_inf_of X, S & inf X = "/\"(X, T))
by YELLOW_0:63;
scheme
ProductSupsInheriting { I() -> non empty set, J,K() -> Poset-yielding
non-Empty ManySortedSet of I(), P[set, set] }: for X being Subset of product K(
) st P[X, product K()] holds product K() inherits_sup_of X, product J()
provided
A1: for X being Subset of product K() st P[X, product K()] for i being
Element of I() holds P[pi(X, i), K().i] and
A2: for i being Element of I() holds K().i is full SubRelStr of J().i and
A3: for i being Element of I(), X being Subset of K().i st P[X, K().i]
holds K().i inherits_sup_of X, J().i
proof
let X be Subset of product K() such that
A4: P[X, product K()] and
A5: ex_sup_of X, product J();
product K() is SubRelStr of product J() by A2,Th36;
then the carrier of product K() c= the carrier of product J() by
YELLOW_0:def 13;
then reconsider Y = X as Subset of product J() by XBOOLE_1:1;
set f = "\/"(X, product J());
A6: now
let i be Element of I();
A7: ex_sup_of pi(Y,i), J().i by A5,Th30;
K().i inherits_sup_of pi(X, i), J().i by A1,A3,A4;
then sup pi(Y,i) in the carrier of K().i by A7;
hence f.i is Element of K().i by A5,Th32;
end;
dom f = I() by WAYBEL_3:27;
then "\/"(X, product J()) is Element of product K() by A6,WAYBEL_3:27;
hence thesis;
end;
scheme
PowerSupsInheriting { I() -> non empty set, L() -> non empty Poset, S() ->
non empty full SubRelStr of L(), P[set, set] }: for X being Subset of S()|^I()
st P[X, S()|^I()] holds S()|^I() inherits_sup_of X, L()|^I()
provided
A1: for X being Subset of S()|^I() st P[X, S()|^I()] for i being Element
of I() holds P[pi(X, i), S()] and
A2: for X being Subset of S() st P[X, S()] holds S() inherits_sup_of X, L()
proof
reconsider K = I() --> S(), J = I() --> L() as Poset-yielding non-Empty
ManySortedSet of I();
A3: now
let X be Subset of product K such that
A4: P[X, product K];
let i be Element of I();
K.i = S() by FUNCOP_1:7;
hence P[pi(X, i), K.i] by A1,A4;
end;
A5: now
let i be Element of I(), X be Subset of K.i such that
A6: P[X, K.i];
A7: J.i = L() by FUNCOP_1:7;
K.i = S() by FUNCOP_1:7;
hence K.i inherits_sup_of X, J.i by A2,A6,A7;
end;
A8: now
let i be Element of I();
J.i = L() by FUNCOP_1:7;
hence K.i is full SubRelStr of J.i by FUNCOP_1:7;
end;
for X being Subset of product K st P[X, product K] holds product K
inherits_sup_of X, product J from ProductSupsInheriting(A3,A8,A5);
hence thesis;
end;
scheme
ProductInfsInheriting { I() -> non empty set, J,K() -> Poset-yielding
non-Empty ManySortedSet of I(), P[set, set] }: for X being Subset of product K(
) st P[X, product K()] holds product K() inherits_inf_of X, product J()
provided
A1: for X being Subset of product K() st P[X, product K()] for i being
Element of I() holds P[pi(X, i), K().i] and
A2: for i being Element of I() holds K().i is full SubRelStr of J().i and
A3: for i being Element of I(), X being Subset of K().i st P[X, K().i]
holds K().i inherits_inf_of X, J().i
proof
let X be Subset of product K() such that
A4: P[X, product K()] and
A5: ex_inf_of X, product J();
product K() is SubRelStr of product J() by A2,Th36;
then the carrier of product K() c= the carrier of product J() by
YELLOW_0:def 13;
then reconsider Y = X as Subset of product J() by XBOOLE_1:1;
set f = "/\"(X, product J());
A6: now
let i be Element of I();
A7: ex_inf_of pi(Y,i), J().i by A5,Th31;
K().i inherits_inf_of pi(X, i), J().i by A1,A3,A4;
then inf pi(Y,i) in the carrier of K().i by A7;
hence f.i is Element of K().i by A5,Th33;
end;
dom f = I() by WAYBEL_3:27;
then "/\"(X, product J()) is Element of product K() by A6,WAYBEL_3:27;
hence thesis;
end;
scheme
PowerInfsInheriting { I() -> non empty set, L() -> non empty Poset, S() ->
non empty full SubRelStr of L(), P[set, set] }: for X being Subset of S()|^I()
st P[X, S()|^I()] holds S()|^I() inherits_inf_of X, L()|^I()
provided
A1: for X being Subset of S()|^I() st P[X, S()|^I()] for i being Element
of I() holds P[pi(X, i), S()] and
A2: for X being Subset of S() st P[X, S()] holds S() inherits_inf_of X, L()
proof
reconsider K = I() --> S(), J = I() --> L() as Poset-yielding non-Empty
ManySortedSet of I();
A3: now
let X be Subset of product K such that
A4: P[X, product K];
let i be Element of I();
K.i = S() by FUNCOP_1:7;
hence P[pi(X, i), K.i] by A1,A4;
end;
A5: now
let i be Element of I(), X be Subset of K.i such that
A6: P[X, K.i];
A7: J.i = L() by FUNCOP_1:7;
K.i = S() by FUNCOP_1:7;
hence K.i inherits_inf_of X, J.i by A2,A6,A7;
end;
A8: now
let i be Element of I();
J.i = L() by FUNCOP_1:7;
hence K.i is full SubRelStr of J.i by FUNCOP_1:7;
end;
for X being Subset of product K st P[X, product K] holds product K
inherits_inf_of X, product J from ProductInfsInheriting(A3,A8,A5);
hence thesis;
end;
registration
let I be set;
let L be non empty RelStr;
let X be non empty Subset of L|^I;
let i be set;
cluster pi(X,i) -> non empty;
coherence
proof
reconsider Y = X as non empty Subset of product (I --> L);
set f = the Element of Y;
reconsider f as Function;
f.i in pi(X,i) by CARD_3:def 6;
hence thesis;
end;
end;
theorem
for L being non empty Poset for S being directed-sups-inheriting non
empty full SubRelStr of L for X be non empty set holds S|^X is
directed-sups-inheriting SubRelStr of L|^X
proof
let L be non empty Poset;
let S be directed-sups-inheriting non empty full SubRelStr of L;
let X be non empty set;
reconsider SX = S|^X as full non empty SubRelStr of L|^X by Th38;
defpred P[set, non empty reflexive RelStr] means $1 is directed non empty
Subset of $2;
A1: now
let A be Subset of S|^X;
assume P[A,S|^X];
then reconsider B = A as directed non empty Subset of S|^X;
let i be Element of X;
(X --> S).i = S by FUNCOP_1:7;
then pi(B, i) is directed non empty Subset of S by Th34;
hence P[pi(A, i),S];
end;
A2: now
let X be Subset of S;
assume P[X,S];
then ex_sup_of X,L implies ex_sup_of X, S & sup X = "\/"(X, L) by
WAYBEL_0:7;
hence S inherits_sup_of X, L;
end;
SX is directed-sups-inheriting
proof
let A be directed Subset of SX;
for A being Subset of S|^X st P[A,S|^X] holds S|^X inherits_sup_of A,
L|^X from PowerSupsInheriting(A1,A2);
then A <> {} implies S|^X inherits_sup_of A, L|^X;
hence thesis;
end;
hence thesis;
end;
registration
let I be non empty set;
let J be RelStr-yielding non-Empty ManySortedSet of I;
let X be non empty Subset of product J;
let i be set;
cluster pi(X,i) -> non empty;
coherence
proof
set f = the Element of X;
reconsider f as Function;
f.i in pi(X,i) by CARD_3:def 6;
hence thesis;
end;
end;
theorem Th42:
for X being non empty set for L being up-complete non empty
Poset holds L|^X is up-complete
proof
let X be non empty set;
let L be up-complete non empty Poset;
now
let A be non empty directed Subset of L|^X;
reconsider B = A as non empty directed Subset of product (X --> L);
now
let x be Element of X;
A1: (X --> L).x = L by FUNCOP_1:7;
pi(B,x) is directed non empty by Th34;
hence ex_sup_of pi(A,x), (X --> L).x by A1,WAYBEL_0:75;
end;
hence ex_sup_of A,L|^X by Th30;
end;
hence thesis by WAYBEL_0:75;
end;
registration
let L be up-complete non empty Poset;
let X be non empty set;
cluster L|^X -> up-complete;
coherence by Th42;
end;
begin :: Topological retracts
theorem Th43:
for T being non empty TopSpace, S being non empty SubSpace of T
for f being Function of T,S st f is being_a_retraction holds rng f = the
carrier of S
proof
let T be non empty TopSpace, S be non empty SubSpace of T;
let f be Function of T,S such that
A1: for W being Point of T st W in the carrier of S holds f.W=W;
thus rng f c= the carrier of S;
let x be object;
A2: [#]S = the carrier of S;
[#]T = the carrier of T;
then
A3: the carrier of S c= the carrier of T by A2,PRE_TOPC:def 4;
assume
A4: x in the carrier of S;
then x in the carrier of T by A3;
then
A5: x in dom f by FUNCT_2:def 1;
f.x = x by A1,A3,A4;
hence thesis by A5,FUNCT_1:def 3;
end;
theorem
for T being non empty TopSpace, S being non empty SubSpace of T for f
being continuous Function of T,S st f is being_a_retraction holds f is
idempotent
proof
let T be non empty TopSpace, S be non empty SubSpace of T;
A1: [#]S = the carrier of S;
let f be continuous Function of T,S such that
A2: f is being_a_retraction;
A3: rng f = the carrier of S by A2,Th43;
A4: dom f = the carrier of T by FUNCT_2:def 1;
[#]T = the carrier of T;
then
A5: the carrier of S c= the carrier of T by A1,PRE_TOPC:def 4;
A6: now
let x be object;
assume
A7: x in the carrier of T;
then
A8: f.x in rng f by A4,FUNCT_1:def 3;
(f*f).x = f.(f.x) by A4,A7,FUNCT_1:13;
hence (f*f).x = f.x by A2,A5,A3,A8;
end;
dom (f*f) = the carrier of T by A5,A4,A3,RELAT_1:27;
then f*f = f by A4,A6,FUNCT_1:2;
hence thesis by QUANTAL1:def 9;
end;
theorem Th45:
for T being non empty TopSpace, V being open Subset of T holds
chi(V, the carrier of T) is continuous Function of T, Sierpinski_Space
proof
let T be non empty TopSpace, V be open Subset of T;
reconsider c = chi(V, the carrier of T) as Function of T, Sierpinski_Space
by WAYBEL18:def 9;
A1: c"{0,1} = [#]T by FUNCT_2:40;
c = chi(c"{1}, the carrier of T) by FUNCT_3:40;
then
A2: V = c"{1} by FUNCT_3:38;
A3: c"{} = {}T;
A4: now
let W be Subset of Sierpinski_Space;
assume W is open;
then W in the topology of Sierpinski_Space by PRE_TOPC:def 2;
then W in {{}, {1}, {0,1}} by WAYBEL18:def 9;
hence c"W is open by A2,A3,A1,ENUMSET1:def 1;
end;
[#]Sierpinski_Space <> {};
hence thesis by A4,TOPS_2:43;
end;
theorem
for T being non empty TopSpace, x,y being Element of T st for W being
open Subset of T st y in W holds x in W holds (0,1) --> (y,x) is continuous
Function of Sierpinski_Space, T
proof
let T be non empty TopSpace;
let x,y be Element of T such that
A1: for W being open Subset of T st y in W holds x in W;
A2: the carrier of Sierpinski_Space = {0,{0}} by WAYBEL18:def 9, CARD_1:49;
then reconsider i = (0,{0}) --> (y,x) as Function of Sierpinski_Space, T;
A3: i.1 = x by FUNCT_4:63, CARD_1:49;
A4: not 1 in {0} by TARSKI:def 1;
A5: 0 in {0} by TARSKI:def 1;
A6: 1 in {0,1} by TARSKI:def 2;
A7: i.0 = y by FUNCT_4:63;
A8: now
let W be Subset of T;
assume W is open;
then
A9: y in W & x in W or not y in W & x in W or not y in W & not x in W by A1;
A10: i"W = {} or i"W = {0} or i"W = {1} or i"W = {0,1}
by A2,ZFMISC_1:36, CARD_1:49;
i"W <> {0} by A7,A3,A6,A5,A4,A9,FUNCT_2:38, CARD_1:49;
then i"W in {{}, {1}, {0,1}}
by ENUMSET1:def 1,A10;
then i"W in the topology of Sierpinski_Space by WAYBEL18:def 9;
hence i"W is open by PRE_TOPC:def 2;
end;
[#]T <> {};
hence thesis by A8,TOPS_2:43, CARD_1:49;
end;
theorem
for T being non empty TopSpace, x,y being Element of T for V being
open Subset of T st x in V & not y in V holds chi(V, the carrier of T)*
((0,1) --> (y,x)) = id Sierpinski_Space
proof
let T be non empty TopSpace;
let x,y be Element of T, V be open Subset of T such that
A1: x in V and
A2: not y in V;
reconsider c = chi(V, the carrier of T) as Function of T, Sierpinski_Space
by Th45;
A3: c.x = 1 by A1,FUNCT_3:def 3;
A4: the carrier of Sierpinski_Space = {0,{0}} by WAYBEL18:def 9, CARD_1:49;
then reconsider i = (0,{0}) --> (y,x) as Function of Sierpinski_Space, T;
A5: i.1 = x by FUNCT_4:63, CARD_1:49;
A6: c.y = 0 by A2,FUNCT_3:def 3;
A7: i.0 = y by FUNCT_4:63;
now
thus c*i is Function of Sierpinski_Space, Sierpinski_Space;
let a be Element of Sierpinski_Space;
a = 0 or a = 1 by A4,TARSKI:def 2, CARD_1:49;
hence (c*i).a = a by A7,A5,A3,A6,FUNCT_2:15
.= (id Sierpinski_Space).a;
end;
hence thesis by FUNCT_2:63, CARD_1:49;
end;
theorem
for T being non empty 1-sorted, V,W being Subset of T for S being
TopAugmentation of BoolePoset{0}
for f, g being Function of T, S st f = chi(V,
the carrier of T) & g = chi(W, the carrier of T) holds V c= W iff f <= g
proof
let T be non empty 1-sorted, V,W be Subset of T;
let S be TopAugmentation of BoolePoset{0};
let c1, c2 be Function of T, S such that
A1: c1 = chi(V, the carrier of T) and
A2: c2 = chi(W, the carrier of T);
A3: the RelStr of S = BoolePoset{0} by YELLOW_9:def 4;
hereby
assume
A4: V c= W;
now
let z be set;
assume z in the carrier of T;
then reconsider x = z as Element of T;
reconsider a = c1.x, b = c2.x as Element of BoolePoset{0} by A3;
x in V & x in W or not x in V by A4;
then c1.x = 1 & c2.x = 1 or c1.x = 0 by A1,A2,FUNCT_3:def 3;
then c1.x c= c2.x;
then a <= b by YELLOW_1:2;
hence ex a,b being Element of S st a = c1.z & b = c2.z & a <= b by A3,
YELLOW_0:1;
end;
hence c1 <= c2;
end;
assume
A5: c1 <= c2;
let x be object;
assume that
A6: x in V and
A7: not x in W;
reconsider x as Element of T by A6;
A8: c2.x = 0 by A2,A7,FUNCT_3:def 3;
A9: 0 c= {0};
reconsider a = c1.x, b = c2.x as Element of BoolePoset{0} by A3;
ex a,b being Element of S st a = c1.x & b = c2.x & a <= b by A5;
then
A10: a <= b by A3,YELLOW_0:1;
c1.x = 1 by A1,A6,FUNCT_3:def 3;
then {0} c= 0 by A8,A10,YELLOW_1:2,CARD_1:49;
hence thesis by A9,XBOOLE_0:def 10;
end;
theorem
for L being non empty RelStr, X being non empty set for R being full
non empty SubRelStr of L|^X st for a being set holds a is Element of R iff ex x
being Element of L st a = X --> x holds L, R are_isomorphic
proof
let L be non empty RelStr, X be non empty set;
deffunc F(set) = X --> $1;
consider f being ManySortedSet of the carrier of L such that
A1: for i being Element of L holds f.i = F(i) from PBOOLE:sch 5;
let R be full non empty SubRelStr of L|^X such that
A2: for a being set holds a is Element of R iff ex x being Element of L
st a = X --> x;
A3: rng f c= the carrier of R
proof
let y be object;
assume y in rng f;
then consider x being object such that
A4: x in dom f and
A5: y = f.x by FUNCT_1:def 3;
reconsider x as Element of L by A4;
y = X --> x by A1,A5;
then y is Element of R by A2;
hence thesis;
end;
A6: dom f = the carrier of L by PARTFUN1:def 2;
then reconsider f as Function of L, R by A3,FUNCT_2:2;
A7: f is one-to-one
proof
let x,y be Element of L;
f.y = X --> y by A1;
then
A8: f.y = [:X,{y}:] by FUNCOP_1:def 2;
f.x = X --> x by A1;
then f.x = [:X,{x}:] by FUNCOP_1:def 2;
then f.x = f.y implies {x} = {y} by A8,ZFMISC_1:110;
hence thesis by ZFMISC_1:3;
end;
A9: now
set i = the Element of X;
let x,y be Element of L;
reconsider a = f.x, b = f.y as Element of L|^X by YELLOW_0:58;
reconsider Xx = X --> x, Xy = X --> y as Function of X,L;
reconsider a9 = a, b9 = b as Element of product (X --> L);
A10: (X --> L).i = L by FUNCOP_1:7;
A11: f.y = X --> y by A1;
A12: f.x = X --> x by A1;
hereby
assume
A13: x <= y;
Xx <= Xy
proof
let i be set;
assume
A14: i in X;
then
A15: (X --> y).i = y by FUNCOP_1:7;
(X --> x).i = x by A14,FUNCOP_1:7;
hence thesis by A13,A15;
end;
then a <= b by A12,A11,WAYBEL10:11;
hence f.x <= f.y by YELLOW_0:60;
end;
assume f.x <= f.y;
then a <= b by YELLOW_0:59;
then a9.i <= b9.i by WAYBEL_3:28;
then x <= Xy.i by A12,A11,A10,FUNCOP_1:7;
hence x <= y by FUNCOP_1:7;
end;
take f;
rng f = the carrier of R
proof
thus rng f c= the carrier of R;
let x be object;
assume x in the carrier of R;
then reconsider a = x as Element of R;
consider i being Element of L such that
A16: a = X --> i by A2;
a = f.i by A1,A16;
hence thesis by A6,FUNCT_1:def 3;
end;
hence thesis by A7,A9,WAYBEL_0:66;
end;
theorem
for S,T being non empty TopSpace holds S, T are_homeomorphic iff ex f
being continuous Function of S,T, g being continuous Function of T,S st f*g =
id T & g*f = id S
proof
let S,T be non empty TopSpace;
hereby
assume S, T are_homeomorphic;
then consider f being Function of S,T such that
A1: f is being_homeomorphism;
reconsider f as continuous Function of S,T by A1,TOPS_2:def 5;
A2: rng f = [#]T by A1,TOPS_2:def 5;
reconsider g = f" as continuous Function of T,S by A1,TOPS_2:def 5;
take f,g;
A3: dom f = [#]S by A1,TOPS_2:def 5;
f is one-to-one by A1,TOPS_2:def 5;
hence f*g = id T & g*f = id S by A2,A3,TOPS_2:52;
end;
given f being continuous Function of S,T, g being continuous Function of T,S
such that
A4: f*g = id T and
A5: g*f = id S;
A6: f is onto by A4,FUNCT_2:23;
then
A7: rng f = [#]T by FUNCT_2:def 3;
take f;
A8: dom f = [#]S by FUNCT_2:def 1;
A9: f is one-to-one by A5,FUNCT_2:23;
then g = f qua Function" by A5,A7,FUNCT_2:30
.= f" by A6,A9,TOPS_2:def 4;
hence thesis by A9,A7,A8,TOPS_2:def 5;
end;
theorem Th51:
for T, S, R being non empty TopSpace for f being Function of T,S
, g being Function of S,T, h being Function of S, R st f*g = id S & h is
being_homeomorphism holds (h*f)*(g*(h")) = id R
proof
let T, S, R be non empty TopSpace;
let f be Function of T,S, g be Function of S,T, h be Function of S, R such
that
A1: f*g = id S and
A2: h is being_homeomorphism;
A3: h is one-to-one by A2,TOPS_2:def 5;
A4: rng h = [#]R by A2,TOPS_2:def 5;
thus (h*f)*(g*(h")) = (h*f)*g*(h") by RELAT_1:36
.= h*(id the carrier of S)*(h") by A1,RELAT_1:36
.= h*(h") by FUNCT_2:17
.= id R by A3,A4,TOPS_2:52;
end;
theorem Th52:
for T, S, R being non empty TopSpace st S is_Retract_of T & S, R
are_homeomorphic holds R is_Retract_of T
proof
let T, S, R be non empty TopSpace;
given f being continuous Function of S,T, g being continuous Function of T,S
such that
A1: g*f = id S;
given h being Function of S,R such that
A2: h is being_homeomorphism;
h" is continuous by A2,TOPS_2:def 5;
then reconsider f9 = f*(h") as continuous Function of R,T;
h is continuous by A2,TOPS_2:def 5;
then reconsider g9 = h*g as continuous Function of T,R;
take f9,g9;
thus thesis by A1,A2,Th51;
end;
theorem Th53:
for T being non empty TopSpace, S being non empty SubSpace of T
holds incl(S,T) is continuous
proof
let T be non empty TopSpace, S be non empty SubSpace of T;
incl(S,T) = id S by BORSUK_1:1,YELLOW_9:def 1;
hence thesis by PRE_TOPC:26;
end;
theorem Th54:
for T being non empty TopSpace for S being non empty SubSpace of
T, f being continuous Function of T,S st f is being_a_retraction holds f*incl(S
,T) = id S
proof
let T be non empty TopSpace, S be non empty SubSpace of T;
let f be continuous Function of T,S such that
A1: f is being_a_retraction;
A2: [#]S = the carrier of S;
[#]T = the carrier of T;
then
A3: the carrier of S c= the carrier of T by A2,PRE_TOPC:def 4;
then
A4: incl(S,T) = id the carrier of S by YELLOW_9:def 1;
now
let x be Element of S;
reconsider y = x as Point of T by A3;
thus (f*incl(S,T)).x = f.((incl(S,T)).x) by FUNCT_2:15
.= f.x by A4
.= y by A1
.= (id S).x;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th55:
for T being non empty TopSpace, S being non empty SubSpace of T
st S is_a_retract_of T holds S is_Retract_of T
proof
let T be non empty TopSpace, S be non empty SubSpace of T;
reconsider g = incl(S,T) as continuous Function of S,T by Th53;
given f be continuous Function of T,S such that
A1: f is being_a_retraction;
take g,f;
thus thesis by A1,Th54;
end;
theorem
for R,T being non empty TopSpace holds R is_Retract_of T iff ex S
being non empty SubSpace of T st S is_a_retract_of T & S,R are_homeomorphic
proof
let R,T be non empty TopSpace;
hereby
assume R is_Retract_of T;
then consider f being Function of T,T such that
A1: f is continuous and
A2: f*f = f and
A3: Image f, R are_homeomorphic by WAYBEL18:def 8;
reconsider S = Image f as non empty SubSpace of T;
f = corestr f by WAYBEL18:def 7;
then reconsider f as continuous Function of T,S by A1,WAYBEL18:10;
take S;
A4: [#]T = the carrier of T;
[#]S = the carrier of S;
then the carrier of S c= the carrier of T by A4,PRE_TOPC:def 4;
then reconsider rf = rng f as Subset of T by XBOOLE_1:1;
now
let x be Point of T;
assume x in the carrier of S;
then x in [#](T|rf) by WAYBEL18:def 6;
then x in rng f by PRE_TOPC:def 5;
then ex y being object st y in dom f & x = f.y by FUNCT_1:def 3;
hence f.x = x by A2,FUNCT_1:13;
end;
then f is being_a_retraction;
hence S is_a_retract_of T & S, R are_homeomorphic by A3;
end;
given S being non empty SubSpace of T such that
A5: S is_a_retract_of T and
A6: S,R are_homeomorphic;
thus thesis by A5,A6,Th52,Th55;
end;