:: Retracts and Inheritance
:: by Grzegorz Bancerek
::
:: Received September 7, 1999
:: Copyright (c) 1999-2021 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;
begin :: Poset retracts
::$CT
theorem :: YELLOW16:2
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;
theorem :: YELLOW16:3
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;
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;
end;
theorem :: YELLOW16:4
for f,g being Function st f is idempotent & rng g c= rng f & rng g c=
dom f holds f*g = g;
registration
let S be 1-sorted;
cluster idempotent for Function of S,S;
end;
theorem :: YELLOW16:5
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;
theorem :: YELLOW16:6
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;
theorem :: YELLOW16:7
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;
definition
let S,T be non empty Poset;
let f be Function;
pred f is_a_retraction_of T,S means
:: YELLOW16:def 1
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
:: YELLOW16:def 2
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
:: YELLOW16:def 3
ex f being Function of T,S st f is_a_retraction_of T,S;
pred S is_an_UPS_retract_of T means
:: YELLOW16:def 4
ex f being Function of T,S st f is_an_UPS_retraction_of T,S;
end;
theorem :: YELLOW16:8
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;
theorem :: YELLOW16:9
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;
theorem :: YELLOW16:10
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;
theorem :: YELLOW16:11
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;
theorem :: YELLOW16:12
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;
theorem :: YELLOW16:13
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;
theorem :: YELLOW16:14
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;
theorem :: YELLOW16:15
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;
theorem :: YELLOW16:16
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;
theorem :: YELLOW16:17
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;
theorem :: YELLOW16:18
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;
theorem :: YELLOW16:19
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;
theorem :: YELLOW16:20
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;
theorem :: YELLOW16:21
for L being complete non empty Poset for S being non empty
Poset st S is_a_retract_of L holds S is complete;
theorem :: YELLOW16:22
for L being continuous complete LATTICE for S being non empty
Poset st S is_a_retract_of L holds S is continuous;
theorem :: YELLOW16:23
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;
theorem :: YELLOW16:24
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;
theorem :: YELLOW16:25
for L being continuous complete LATTICE for S being non empty Poset st
S is_an_UPS_retract_of L holds S is continuous;
theorem :: YELLOW16:26
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;
theorem :: YELLOW16:27
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;
theorem :: YELLOW16:28
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;
begin :: Products
definition
let R be Relation;
attr R is Poset-yielding means
:: YELLOW16:def 5
for x being set st x in rng R holds x is Poset;
end;
registration
cluster Poset-yielding -> RelStr-yielding reflexive-yielding for Relation;
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;
end;
registration
let X be set;
let S be Poset;
cluster X --> S -> Poset-yielding;
end;
registration
let I be set;
cluster Poset-yielding non-Empty for ManySortedSet of I;
end;
registration
let I be non empty set;
let J be Poset-yielding non-Empty ManySortedSet of I;
cluster product J -> transitive antisymmetric;
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;
end;
theorem :: YELLOW16:29
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
);
theorem :: YELLOW16:30
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
);
theorem :: YELLOW16:31
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;
theorem :: YELLOW16:32
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;
theorem :: YELLOW16:33
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);
theorem :: YELLOW16:34
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);
theorem :: YELLOW16:35
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;
theorem :: YELLOW16:36
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;
theorem :: YELLOW16:37
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;
theorem :: YELLOW16:38
for L being non empty RelStr, S being non empty SubRelStr of L, X
being set holds S|^X is SubRelStr of L|^X;
theorem :: YELLOW16:39
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;
begin :: Inheritance
definition
let S,T be non empty RelStr, X be set;
pred S inherits_sup_of X,T means
:: YELLOW16:def 6
ex_sup_of X,T implies "\/"(X, T) in the carrier of S;
pred S inherits_inf_of X,T means
:: YELLOW16:def 7
ex_inf_of X,T implies "/\"(X, T) in the carrier of S;
end;
theorem :: YELLOW16:40
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));
theorem :: YELLOW16:41
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));
scheme :: YELLOW16:sch 1
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
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
for i being Element of I() holds K().i is full SubRelStr of J().i and
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;
scheme :: YELLOW16:sch 2
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
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
for X being Subset of S() st P[X, S()] holds S() inherits_sup_of X, L();
scheme :: YELLOW16:sch 3
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
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
for i being Element of I() holds K().i is full SubRelStr of J().i and
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;
scheme :: YELLOW16:sch 4
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
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
for X being Subset of S() st P[X, S()] holds S() inherits_inf_of X, L();
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;
end;
theorem :: YELLOW16:42
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;
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;
end;
theorem :: YELLOW16:43
for X being non empty set for L being up-complete non empty
Poset holds L|^X is up-complete;
registration
let L be up-complete non empty Poset;
let X be non empty set;
cluster L|^X -> up-complete;
end;
begin :: Topological retracts
theorem :: YELLOW16:44
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;
theorem :: YELLOW16:45
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;
theorem :: YELLOW16:46
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;
theorem :: YELLOW16:47
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;
theorem :: YELLOW16:48
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;
theorem :: YELLOW16:49
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;
theorem :: YELLOW16:50
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;
theorem :: YELLOW16:51
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;
theorem :: YELLOW16:52
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;
theorem :: YELLOW16:53
for T, S, R being non empty TopSpace st S is_Retract_of T & S, R
are_homeomorphic holds R is_Retract_of T;
theorem :: YELLOW16:54
for T being non empty TopSpace, S being non empty SubSpace of T
holds incl(S,T) is continuous;
theorem :: YELLOW16:55
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;
theorem :: YELLOW16:56
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;
theorem :: YELLOW16:57
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;