:: Preliminaries to Structures
:: by Library Committee
::
:: Received January 6, 1995
:: Copyright (c) 1995-2026 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, CARD_1, FINSET_1,
RELSET_1;
requirements BOOLE, SUBSET, NUMERALS;
definitions ZFMISC_1;
equalities SUBSET_1;
expansions SUBSET_1;
theorems TARSKI, ZFMISC_1, XBOOLE_0, SUBSET_1, CARD_1, XBOOLE_1;
begin
definition
struct 1-sorted(# carrier -> set #);
end;
definition
let S be 1-sorted;
attr S is empty means
:Def1:
the carrier of S is empty;
end;
registration
cluster strict empty for 1-sorted;
existence
proof
take T = 1-sorted(#{}#);
thus T is strict;
thus the carrier of T is empty;
end;
end;
registration
cluster strict non empty for 1-sorted;
existence
proof
take 1-sorted(#{{}}#);
thus 1-sorted(#{{}}#) is strict;
thus the carrier of 1-sorted(#{{}}#) is non empty;
end;
end;
registration
let S be empty 1-sorted;
cluster the carrier of S -> empty;
coherence by Def1;
end;
registration
let S be non empty 1-sorted;
cluster the carrier of S -> non empty;
coherence by Def1;
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
{};
coherence
proof
{} = {}the carrier of T;
hence thesis;
end;
func [#]T -> Subset of T equals
the carrier of T;
coherence
proof
the carrier of T = [#]the carrier of T;
hence thesis;
end;
end;
registration
let T be 1-sorted;
cluster {}T -> empty;
coherence;
end;
registration
let T be empty 1-sorted;
cluster [#]T -> empty;
coherence;
end;
registration
let T be non empty 1-sorted;
cluster [#]T -> non empty;
coherence;
end;
registration
let S be non empty 1-sorted;
cluster non empty for Subset of S;
existence
proof
take [#]S;
thus thesis;
end;
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
id the carrier of S;
coherence;
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
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;
existence
proof
set A = the non empty set, a = the Element of A;
take ZeroStr(#A,a#);
thus ZeroStr(#A,a#) is strict;
thus the carrier of ZeroStr(#A,a#) is non empty;
end;
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
the ZeroF of S;
coherence;
end;
definition
let S be OneStr;
func 1.S -> Element of S equals
the OneF of S;
coherence;
end;
definition
let S be ZeroOneStr;
attr S is degenerated means
:Def8:
0.S = 1.S;
end;
definition
let IT be 1-sorted;
attr IT is trivial means
:Def9:
the carrier of IT is trivial;
end;
registration
cluster empty -> trivial for 1-sorted;
coherence;
cluster non trivial -> non empty for 1-sorted;
coherence;
end;
definition
let S be 1-sorted;
redefine attr S is trivial means :: redefines trivial (STRUCT_0, definition)
:Def10:
for x,y being Element of S holds x = y;
compatibility
proof set I = the carrier of S;
per cases;
suppose
I is non empty;
thus S is trivial implies for x,y being Element of I holds x = y
proof
assume
A2: I is trivial;
let x,y be Element of I;
thus thesis by A2;
end;
assume
A3: for x,y being Element of I holds x = y;
let x,y be object;
thus thesis by A3;
end;
suppose
A4: I is empty;
for x,y being Element of I holds x = y
proof
let x, y be Element of I;
thus x = {} by A4,SUBSET_1:def 1
.= y by A4,SUBSET_1:def 1;
end;
hence thesis by A4;
end;
end;
end;
registration
cluster non degenerated -> non trivial for ZeroOneStr;
coherence;
end;
registration
cluster trivial non empty strict for 1-sorted;
existence
proof
take 1-sorted (#1#);
thus thesis by CARD_1:49;
end;
cluster non trivial strict for 1-sorted;
existence
proof
take Y = 1-sorted (#2#);
reconsider x=0, y=1 as Element of Y by CARD_1:50,TARSKI:def 2;
x <> y;
hence thesis;
end;
end;
registration
let S be non trivial 1-sorted;
cluster the carrier of S -> non trivial;
coherence by Def9;
end;
registration
let S be trivial 1-sorted;
cluster the carrier of S -> trivial;
coherence by Def9;
end;
begin :: Finite 1-sorted Structures
definition
let S be 1-sorted;
attr S is finite means
:Def11:
the carrier of S is finite;
end;
registration
cluster strict finite non empty for 1-sorted;
existence
proof
take 1-sorted(#{{}}#);
thus thesis;
end;
end;
registration
let S be finite 1-sorted;
cluster the carrier of S -> finite;
coherence by Def11;
end;
registration
cluster -> finite for empty 1-sorted;
coherence;
end;
notation
let S be 1-sorted;
antonym S is infinite for S is finite;
end;
registration
cluster strict infinite for 1-sorted;
existence
proof
take A = 1-sorted(#the infinite set#);
thus A is strict;
thus the carrier of A is infinite;
end;
end;
registration
let S be infinite 1-sorted;
cluster the carrier of S -> infinite;
coherence by Def11;
end;
registration
cluster -> non empty for infinite 1-sorted;
coherence;
end;
:: from YELLOW_13, 2007.04.12, A.T.
registration
cluster trivial -> finite for 1-sorted;
coherence;
end;
registration
cluster infinite -> non trivial for 1-sorted;
coherence;
end;
definition
let S be ZeroStr, x be Element of S;
attr x is zero means
x = 0.S;
end;
registration
let S be ZeroStr;
cluster 0.S -> zero;
coherence;
end;
registration
cluster strict non degenerated for ZeroOneStr;
existence
proof
take S = ZeroOneStr(#2,In(0,2),In(1,2)#);
0 in 2 by CARD_1:50,TARSKI:def 2;
then 1 in 2 & In(0,2) = 0 by CARD_1:50,SUBSET_1:def 8,TARSKI:def 2;
then 0.S <> 1.S by SUBSET_1:def 8;
hence thesis;
end;
end;
registration
let S be non degenerated ZeroOneStr;
cluster 1.S -> non zero;
coherence by Def8;
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;
coherence;
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
:Def13:
the carrier' of S is empty;
end;
registration
cluster strict empty void for 2-sorted;
existence
proof
take S = 2-sorted(#{},{}#);
thus S is strict;
thus the carrier of S is empty;
thus the carrier' of S is empty;
end;
end;
registration
let S be void 2-sorted;
cluster the carrier' of S -> empty;
coherence by Def13;
end;
registration
cluster strict non empty non void for 2-sorted;
existence
proof
take S = 2-sorted(#{0},{0}#);
thus S is strict;
thus the carrier of S is not empty;
thus the carrier' of S is not empty;
end;
end;
registration
let S be non void 2-sorted;
cluster the carrier' of S -> non empty;
coherence by Def13;
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
(the carrier of X) --> y;
coherence;
end;
registration
let S be ZeroStr;
cluster zero for Element of S;
existence
proof
take 0.S;
thus 0.S = 0.S;
end;
end;
registration
cluster strict non trivial for ZeroStr;
existence
proof
take ZeroStr(#2,In(0,2)#);
0 in 2 & 1 in 2 by CARD_1:50,TARSKI:def 2;
hence thesis;
end;
end;
registration
let S be non trivial ZeroStr;
cluster non zero for Element of S;
existence
proof
consider x,y being Element of S such that
A1: x <> y by Def10;
per cases by A1;
suppose
A2: x <> 0.S;
take x;
thus x <> 0.S by A2;
end;
suppose
A3: y <> 0.S;
take y;
thus y <> 0.S by A3;
end;
end;
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
not 0.S in rng R;
end;
:: 2008.10.12, A.T.
definition
let S be 1-sorted;
func card S -> Cardinal equals
card the carrier of S;
coherence;
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
[#]S \ {0.S};
coherence;
end;
theorem
for S being non empty ZeroStr for u being Element of S holds u in
NonZero S iff u is not zero
by ZFMISC_1:56;
definition
let V be non empty ZeroStr;
redefine attr V is trivial means :: redefines trivial (STRUCT_0, redefinition) → trivial (STRUCT_0, definition)
:Def18:
for u being Element of V holds u = 0.V;
compatibility
proof
thus V is trivial implies for a being Element of V holds a = 0.V;
assume
A1: for a being Element of V holds a = 0.V;
let a,b be Element of V;
thus a = 0.V by A1
.= b by A1;
end;
end;
registration
let V be non trivial ZeroStr;
cluster NonZero V -> non empty;
coherence
proof
ex u being Element of V st u <> 0.V by Def18;
hence thesis by ZFMISC_1:56;
end;
end;
registration
cluster trivial non empty for ZeroStr;
existence
proof
take ZeroStr(#1,In(0,1)#);
thus thesis by CARD_1:49;
end;
end;
registration
let S be trivial non empty ZeroStr;
cluster NonZero S -> empty;
coherence
proof
assume NonZero S is not empty;
then consider x being Element of S such that
A1: x in NonZero S by SUBSET_1:4;
not x in {0.S} by A1,XBOOLE_0:def 5;
then x <> 0.S by TARSKI:def 1;
hence contradiction by Def18;
end;
end;
registration
let S be non empty 1-sorted;
cluster non empty trivial for Subset of S;
existence
proof
{the Element of S} is Subset of S;
hence thesis;
end;
end;
theorem
for F being non degenerated ZeroOneStr holds 1.F in NonZero F
proof
let F be non degenerated ZeroOneStr;
not 1.F in {0.F} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 5;
end;
:: 2011.03.01, A.T.
registration
let S be finite 1-sorted;
cluster card S -> natural;
coherence;
end;
registration
let S be finite non empty 1-sorted;
cluster card S -> non zero for Nat;
coherence;
end;
registration
let T be non trivial 1-sorted;
cluster non trivial for Subset of T;
existence
proof
consider x, y being Element of T such that
A1: x <> y by Def10;
reconsider A = {x,y} as Subset of T;
take A, x, y;
thus x in A by TARSKI:def 2;
thus y in A by TARSKI:def 2;
thus thesis by A1;
end;
end;
:: 2011.04.05, A.T.
theorem :: COMPOS_1:56
for S being ZeroStr holds not 0.S in NonZero S
proof let S be ZeroStr;
assume 0.S in NonZero S;
then not 0.S in {0.S} by XBOOLE_0:def 5;
hence thesis by TARSKI:def 1;
end;
theorem :: COMPOS_1:160
for S being non empty ZeroStr
holds the carrier of S = {0.S} \/ NonZero S by XBOOLE_1:45;
:: 2011.05.02, A.T.
definition let C be set, X be 1-sorted;
attr X is C-element means
:Def19: the carrier of X is C-element;
end;
registration let C be Cardinal;
cluster C-element for 1-sorted;
existence
proof
take X = 1-sorted(#the C-element set#);
thus the carrier of X is C-element;
end;
end;
registration let C be Cardinal, X be C-element 1-sorted;
cluster the carrier of X -> C-element;
coherence by Def19;
end;
registration
cluster empty -> 0-element for 1-sorted;
coherence;
cluster 0-element -> empty for 1-sorted;
coherence;
cluster non empty trivial -> 1-element for 1-sorted;
coherence;
cluster 1-element -> non empty trivial for 1-sorted;
coherence;
end;
:: Feasibility, 2011.11.15, A.T.
definition let S be 2-sorted;
attr S is feasible means
the carrier of S is empty implies the carrier' of S is empty;
end;
registration
cluster non empty -> feasible for 2-sorted;
coherence;
cluster void -> feasible for 2-sorted;
coherence;
cluster empty feasible -> void for 2-sorted;
coherence;
cluster non void feasible -> non empty for 2-sorted;
coherence;
end;
definition let S be 2-sorted;
attr S is trivial' means
:Def21: the carrier' of S is trivial;
end;
registration
cluster strict non empty non void trivial trivial' for 2-sorted;
existence
proof
take S = 2-sorted(#{0},{0}#);
thus S is strict;
thus S is not empty;
thus S is not void;
thus S is trivial;
thus the carrier' of S is trivial;
end;
end;
registration let S be trivial' 2-sorted;
cluster the carrier' of S ->trivial;
coherence by Def21;
end;
registration
cluster non trivial' for 2-sorted;
existence
proof
take S = 2-sorted(#1,{0,1}#);
0 in {0,1} & 1 in {0,1} by TARSKI:def 2;
hence thesis by ZFMISC_1:def 10;
end;
end;
registration let S be non trivial' 2-sorted;
cluster the carrier' of S -> non trivial;
coherence by Def21;
end;
registration
cluster void -> trivial' for 2-sorted;
coherence;
cluster non trivial -> non empty for 1-sorted;
coherence;
end;
definition
let x be object, S be 1-sorted;
func In(x,S) -> Element of S equals
In(x,the carrier of S);
coherence;
end;