:: Preliminaries to Structures :: by Library Committee :: :: Received January 6, 1995 :: Copyright (c) 1995-2018 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 XBOOLE_0, SUBSET_1, SETFAM_1, FUNCT_1, FINSEQ_1, PBOOLE, RELAT_1, NAT_1, PARTFUN1, SUPINF_2, MESFUNC1, ZFMISC_1, CARD_1, FINSET_1, XCMPLX_0, FUNCT_7, FUNCOP_1, VALUED_0, BINOP_1, STRUCT_0, ORDINAL1, MSUALG_6; notations TARSKI, XBOOLE_0, SUBSET_1, DOMAIN_1, SETFAM_1, FINSET_1, ORDINAL1, CARD_1, RELAT_1, XCMPLX_0, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, NAT_1, FINSEQ_1, FUNCOP_1, ZFMISC_1, PBOOLE, FUNCT_7; constructors PARTFUN1, PBOOLE, ZFMISC_1, FUNCT_7, SETFAM_1, RELSET_1, XCMPLX_0, DOMAIN_1; registrations XBOOLE_0, FUNCT_1, FUNCT_2, ZFMISC_1, ORDINAL1, CARD_1, FINSET_1, RELSET_1; requirements BOOLE, SUBSET, NUMERALS; begin definition struct 1-sorted(# carrier -> set #); end; definition let S be 1-sorted; attr S is empty means :: STRUCT_0:def 1 the carrier of S is empty; end; registration cluster strict empty for 1-sorted; end; registration cluster strict non empty for 1-sorted; end; registration let S be empty 1-sorted; cluster the carrier of S -> empty; end; registration let S be non empty 1-sorted; cluster the carrier of S -> non empty; end; definition let S be 1-sorted; mode Element of S is Element of the carrier of S; mode Subset of S is Subset of the carrier of S; mode Subset-Family of S is Subset-Family of the carrier of S; end; :: Added by AK on 2005.09.22 :: Moved from ALG_1, GROUP_6, PRE_TOPC, POLYNOM1 definition let S be 1-sorted, X be set; mode Function of S,X is Function of the carrier of S, X; mode Function of X,S is Function of X, the carrier of S; end; definition let S, T be 1-sorted; mode Function of S,T is Function of the carrier of S, the carrier of T; end; :: from PRE_TOPC, 2006.12.02, AT definition let T be 1-sorted; func {}T -> Subset of T equals :: STRUCT_0:def 2 {}; func [#]T -> Subset of T equals :: STRUCT_0:def 3 the carrier of T; end; registration let T be 1-sorted; cluster {}T -> empty; end; registration let T be empty 1-sorted; cluster [#]T -> empty; end; registration let T be non empty 1-sorted; cluster [#]T -> non empty; end; registration let S be non empty 1-sorted; cluster non empty for Subset of S; end; ::Moved from TOPREAL1 on 2005.09.22 definition let S be 1-sorted; mode FinSequence of S is FinSequence of the carrier of S; end; ::Moved from YELLOW18, AK, 21.02.2006 definition let S be 1-sorted; mode ManySortedSet of S is ManySortedSet of the carrier of S; end; ::Moved from GRCAT_1, AK, 16.01.2007 definition let S be 1-sorted; func id S -> Function of S,S equals :: STRUCT_0:def 4 id the carrier of S; end; ::Moved from NORMSP_1, AK, 14.02.2007 definition let S be 1-sorted; mode sequence of S is sequence of the carrier of S; end; ::Moved from NFCONT_1, AK, 14.02.2007 definition let S be 1-sorted, X be set; mode PartFunc of S,X is PartFunc of the carrier of S, X; mode PartFunc of X,S is PartFunc of X, the carrier of S; end; definition let S,T be 1-sorted; mode PartFunc of S,T is PartFunc of the carrier of S,the carrier of T; end; ::Moved from RLVECT_1, 2007.02.19, A.T. definition let S be 1-sorted; let x be object; pred x in S means :: STRUCT_0:def 5 x in the carrier of S; end; :: Pointed structures definition struct (1-sorted) ZeroStr (# carrier -> set, ZeroF -> Element of the carrier #); end; registration cluster strict non empty for ZeroStr; end; definition struct (1-sorted) OneStr(# carrier -> set, OneF -> Element of the carrier #); end; definition struct (ZeroStr,OneStr) ZeroOneStr(# carrier -> set, ZeroF -> Element of the carrier, OneF -> Element of the carrier #); end; definition let S be ZeroStr; func 0.S -> Element of S equals :: STRUCT_0:def 6 the ZeroF of S; end; definition let S be OneStr; func 1.S -> Element of S equals :: STRUCT_0:def 7 the OneF of S; end; definition let S be ZeroOneStr; attr S is degenerated means :: STRUCT_0:def 8 0.S = 1.S; end; definition let IT be 1-sorted; attr IT is trivial means :: STRUCT_0:def 9 the carrier of IT is trivial; end; registration cluster empty -> trivial for 1-sorted; cluster non trivial -> non empty for 1-sorted; end; definition let S be 1-sorted; redefine attr S is trivial means :: STRUCT_0:def 10 for x,y being Element of S holds x = y; end; registration cluster non degenerated -> non trivial for ZeroOneStr; end; registration cluster trivial non empty strict for 1-sorted; cluster non trivial strict for 1-sorted; end; registration let S be non trivial 1-sorted; cluster the carrier of S -> non trivial; end; registration let S be trivial 1-sorted; cluster the carrier of S -> trivial; end; begin :: Finite 1-sorted Structures definition let S be 1-sorted; attr S is finite means :: STRUCT_0:def 11 the carrier of S is finite; end; registration cluster strict finite non empty for 1-sorted; end; registration let S be finite 1-sorted; cluster the carrier of S -> finite; end; registration cluster -> finite for empty 1-sorted; end; notation let S be 1-sorted; antonym S is infinite for S is finite; end; registration cluster strict infinite for 1-sorted; end; registration let S be infinite 1-sorted; cluster the carrier of S -> infinite; end; registration cluster -> non empty for infinite 1-sorted; end; :: from YELLOW_13, 2007.04.12, A.T. registration cluster trivial -> finite for 1-sorted; end; registration cluster infinite -> non trivial for 1-sorted; end; definition let S be ZeroStr, x be Element of S; attr x is zero means :: STRUCT_0:def 12 x = 0.S; end; registration let S be ZeroStr; cluster 0.S -> zero; end; registration cluster strict non degenerated for ZeroOneStr; end; registration let S be non degenerated ZeroOneStr; cluster 1.S -> non zero; end; definition let S be 1-sorted; mode Cover of S is Cover of the carrier of S; end; :: from RING_1, 2008.06.19, A.T. (needed in TEX_2) registration let S be 1-sorted; cluster [#]S -> non proper; end; begin :: 2-sorted structures, 2008.07.02, A.T. definition struct(1-sorted) 2-sorted(#carrier,carrier' -> set#); end; definition let S be 2-sorted; attr S is void means :: STRUCT_0:def 13 the carrier' of S is empty; end; registration cluster strict empty void for 2-sorted; end; registration let S be void 2-sorted; cluster the carrier' of S -> empty; end; registration cluster strict non empty non void for 2-sorted; end; registration let S be non void 2-sorted; cluster the carrier' of S -> non empty; end; :: from BORSUK_1, 2008.07.07, A.T. definition let X be 1-sorted, Y be non empty 1-sorted, y be Element of Y; func X --> y -> Function of X,Y equals :: STRUCT_0:def 14 (the carrier of X) --> y; end; registration let S be ZeroStr; cluster zero for Element of S; end; registration cluster strict non trivial for ZeroStr; end; registration let S be non trivial ZeroStr; cluster non zero for Element of S; end; :: comp. NDIFF_1, 2008.08.29, A.T. definition let X be set, S be ZeroStr, R be Relation of X, the carrier of S; attr R is non-zero means :: STRUCT_0:def 15 not 0.S in rng R; end; :: 2008.10.12, A.T. definition let S be 1-sorted; func card S -> Cardinal equals :: STRUCT_0:def 16 card the carrier of S; end; :: 2009.01.11, A.K. definition let S be 1-sorted; mode UnOp of S is UnOp of the carrier of S; mode BinOp of S is BinOp of the carrier of S; end; :: 2009.01.24, A.T. definition let S be ZeroStr; func NonZero S -> Subset of S equals :: STRUCT_0:def 17 [#]S \ {0.S}; end; theorem :: STRUCT_0:1 for S being non empty ZeroStr for u being Element of S holds u in NonZero S iff u is not zero; definition let V be non empty ZeroStr; redefine attr V is trivial means :: STRUCT_0:def 18 for u being Element of V holds u = 0.V; end; registration let V be non trivial ZeroStr; cluster NonZero V -> non empty; end; registration cluster trivial non empty for ZeroStr; end; registration let S be trivial non empty ZeroStr; cluster NonZero S -> empty; end; registration let S be non empty 1-sorted; cluster non empty trivial for Subset of S; end; theorem :: STRUCT_0:2 for F being non degenerated ZeroOneStr holds 1.F in NonZero F; :: 2011.03.01, A.T. registration let S be finite 1-sorted; cluster card S -> natural; end; registration let S be finite non empty 1-sorted; cluster card S -> non zero for Nat; end; registration let T be non trivial 1-sorted; cluster non trivial for Subset of T; end; :: 2011.04.05, A.T. theorem :: STRUCT_0:3 :: COMPOS_1:56 for S being ZeroStr holds not 0.S in NonZero S; theorem :: STRUCT_0:4 :: COMPOS_1:160 for S being non empty ZeroStr holds the carrier of S = {0.S} \/ NonZero S; :: 2011.05.02, A.T. definition let C be set, X be 1-sorted; attr X is C-element means :: STRUCT_0:def 19 the carrier of X is C-element; end; registration let C be Cardinal; cluster C-element for 1-sorted; end; registration let C be Cardinal, X be C-element 1-sorted; cluster the carrier of X -> C-element; end; registration cluster empty -> 0-element for 1-sorted; cluster 0-element -> empty for 1-sorted; cluster non empty trivial -> 1-element for 1-sorted; cluster 1-element -> non empty trivial for 1-sorted; end; :: Feasibility, 2011.11.15, A.T. definition let S be 2-sorted; attr S is feasible means :: STRUCT_0:def 20 the carrier of S is empty implies the carrier' of S is empty; end; registration cluster non empty -> feasible for 2-sorted; cluster void -> feasible for 2-sorted; cluster empty feasible -> void for 2-sorted; cluster non void feasible -> non empty for 2-sorted; end; definition let S be 2-sorted; attr S is trivial' means :: STRUCT_0:def 21 the carrier' of S is trivial; end; registration cluster strict non empty non void trivial trivial' for 2-sorted; end; registration let S be trivial' 2-sorted; cluster the carrier' of S ->trivial; end; registration cluster non trivial' for 2-sorted; end; registration let S be non trivial' 2-sorted; cluster the carrier' of S -> non trivial; end; registration cluster void -> trivial' for 2-sorted; cluster non trivial -> non empty for 1-sorted; end; definition let x be object, S be 1-sorted; func In(x,S) -> Element of S equals :: STRUCT_0:def 22 In(x,the carrier of S); end;