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;