Volume 11, 1999

University of Bialystok

Copyright (c) 1999 Association of Mizar Users

### The abstract of the Mizar article:

### Retracts and Inheritance

**by****Grzegorz Bancerek**- Received September 7, 1999
- MML identifier: YELLOW16

- [ Mizar article, MML identifier index ]

environ vocabulary RELAT_1, SEQ_1, ORDERS_1, YELLOW_0, FUNCT_1, CAT_1, RELAT_2, WAYBEL_0, SEQM_3, PRE_TOPC, FUNCOP_1, QUANTAL1, ORDINAL2, BINOP_1, BOOLE, GROUP_6, LATTICES, FUNCT_3, BORSUK_1, WAYBEL_1, WELLORD1, BHSP_3, YELLOW_1, WAYBEL_3, GROUP_1, CARD_3, PBOOLE, LATTICE3, FUNCT_4, RLVECT_2, SUBSET_1, WAYBEL18, YELLOW_9, T_0TOPSP, TOPS_2, YELLOW16; notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_3, FUNCT_7, STRUCT_0, CARD_3, ZF_FUND1, PBOOLE, PRALG_1, PRE_CIRC, FUNCT_4, WELLORD1, ORDERS_1, LATTICE3, GRCAT_1, 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 PRE_CIRC, FUNCT_7, ENUMSET1, ORDERS_3, WAYBEL_1, T_0TOPSP, ZF_FUND1, QUANTAL1, GRCAT_1, TOPS_2, YELLOW_9, NATTRA_1, TOLER_1, WAYBEL18, BORSUK_1; clusters STRUCT_0, WAYBEL_0, WAYBEL_3, RELSET_1, YELLOW_1, LATTICE3, BORSUK_2, WAYBEL10, WAYBEL17, YELLOW_0, FUNCT_1, SUBSET_1, PRE_TOPC, TOPS_1, YELLOW_2, WAYBEL18, XBOOLE_0; requirements SUBSET, BOOLE; begin :: Poset retracts theorem :: YELLOW16:1 for a,b being Relation holds a*b = a(#)b; 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 f',g' being Function of X, the carrier of L st f' = f & g' = g & f <= g holds f' <= g'; 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 f',g' being Function of X, the carrier of L st f' = f & g' = g & f' <= g' holds f <= g; definition let S be non empty RelStr; let T be non empty reflexive antisymmetric RelStr; cluster directed-sups-preserving monotone map 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; definition let S be 1-sorted; cluster idempotent map 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 map of L, L st f is idempotent directed-sups-preserving holds Image f is directed-sups-inheriting; canceled; theorem :: YELLOW16:8 for S, T being non empty RelStr, f being map of T,S, g being map of S,T holds f*g = id S implies rng f = the carrier of S; theorem :: YELLOW16:9 for T being non empty RelStr, S being non empty SubRelStr of T for f being map of T,S holds f*incl(S,T) = id S implies f is idempotent map 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 map 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 map of T,S & ex g being directed-sups-preserving map 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 map 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 map of T,S st f is_an_UPS_retraction_of T,S; end; theorem :: YELLOW16:10 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:11 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:12 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:13 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:14 for S,T being non empty Poset, f being Function st f is_a_retraction_of T,S holds f is idempotent map of T,T; theorem :: YELLOW16:15 for T,S being non empty Poset, f being map of T,T st f is_a_retraction_of T,S holds Image f = the RelStr of S; theorem :: YELLOW16:16 for T being up-complete (non empty Poset) for S being non empty Poset, f being map of T,T st f is_a_retraction_of T,S holds f is directed-sups-preserving projection; theorem :: YELLOW16:17 for S,T being non empty reflexive transitive RelStr for f being map of S,T holds f is isomorphic iff f is monotone & ex g being monotone map of T,S st f*g = id T & g*f = id S; theorem :: YELLOW16:18 for S,T being non empty Poset holds S,T are_isomorphic iff ex f being monotone map of S,T, g being monotone map of T,S st f*g = id T & g*f = id S; theorem :: YELLOW16:19 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:20 for T,S being non empty Poset for f being monotone map of T,S, g being monotone map of S,T st f*g = id S ex h being projection map of T,T st h = g*f & h|the carrier of Image h = id Image h & S, Image h are_isomorphic; theorem :: YELLOW16:21 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 map of T,T st h is_a_retraction_of T, Image h & S, Image h are_isomorphic; theorem :: YELLOW16:22 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:23 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:24 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:25 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:26 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:27 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:28 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:29 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:30 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; definition cluster Poset-yielding -> RelStr-yielding reflexive-yielding 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; definition let X be set; let S be Poset; cluster X --> S -> Poset-yielding; end; definition let I be set; cluster Poset-yielding non-Empty ManySortedSet of I; end; definition 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:31 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:32 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:33 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:34 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:35 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:36 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:37 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:38 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:39 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:40 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:41 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:42 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:43 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 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 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 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 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(); definition 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:44 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; definition 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:45 for X being non empty set for L being up-complete (non empty Poset) holds L|^X is up-complete; definition let L be up-complete (non empty Poset); let X be non empty set; cluster L|^X -> up-complete; end; begin :: Topological retracts definition let T be TopSpace; cluster the topology of T -> non empty; end; theorem :: YELLOW16:46 for T being non empty TopSpace, S being non empty SubSpace of T for f being ::continuous map of T,S st f is_a_retraction holds rng f = the carrier of S; theorem :: YELLOW16:47 for T being non empty TopSpace, S being non empty SubSpace of T for f being continuous map of T,S st f is_a_retraction holds f is idempotent; theorem :: YELLOW16:48 for T being non empty TopSpace, V being open Subset of T holds chi(V, the carrier of T) is continuous map of T, Sierpinski_Space; theorem :: YELLOW16:49 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 map of Sierpinski_Space, T; theorem :: YELLOW16:50 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:51 for T being non empty 1-sorted, V,W being Subset of T for S being TopAugmentation of BoolePoset 1 for f, g being map 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:52 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:53 for S,T being non empty TopSpace holds S, T are_homeomorphic iff ex f being continuous map of S,T, g being continuous map of T,S st f*g = id T & g*f = id S; theorem :: YELLOW16:54 for T, S, R being non empty TopSpace for f being map of T,S, g being map of S,T, h being map of S, R st f*g = id S & h is_homeomorphism holds (h*f)*(g*(h")) = id R; theorem :: YELLOW16:55 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:56 for T being non empty TopSpace, S being non empty SubSpace of T holds incl(S,T) is continuous; theorem :: YELLOW16:57 for T being non empty TopSpace for S being non empty SubSpace of T, f being continuous map of T,S st f is_a_retraction holds f*incl(S,T) = id S; theorem :: YELLOW16:58 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:59 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;

Back to top