:: 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;