:: Preliminaries to Structures
:: by Library Committee
::
:: Received January 6, 1995
:: Copyright (c) 1995-2021 Association of Mizar Users

definition

attr c₁ is strict ;
struct 1-sorted -> ;
aggr 1-sorted(# carrier #) -> 1-sorted ;
sel carrier c₁ -> set ;

end;

definition

let S be 1-sorted ;

attr S is empty means :Def1: :: STRUCT_0:def 1
the carrier of S is empty ;

end;

:: deftheorem Def1 defines empty STRUCT_0:def 1 :
for S being 1-sorted holds
( S is empty iff the carrier of S is empty );

registration

cluster strict empty for 1-sorted ;

existence
ex b₁ being 1-sorted st
( b₁ is strict & b₁ is empty )

proof end;

end;

registration

cluster strict non empty for 1-sorted ;

existence
ex b₁ being 1-sorted st
( b₁ is strict & not b₁ is empty )

proof end;

end;

registration

let S be empty 1-sorted ;

cluster the carrier of S -> empty ;

coherence
the carrier of S is empty by Def1;

end;

registration

let S be non empty 1-sorted ;

cluster the carrier of S -> non empty ;

coherence
not the carrier of S is empty 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 ;
let 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
{} ;

coherence
{} is Subset of T

proof end;

func [#] T -> Subset of T equals :: STRUCT_0:def 3
the carrier of T;

coherence
the carrier of T is Subset of T

proof end;

end;

:: deftheorem defines {} STRUCT_0:def 2 :
for T being 1-sorted holds {} T = {} ;

:: deftheorem defines [#] STRUCT_0:def 3 :
for T being 1-sorted holds [#] T = the carrier of T;

registration

let T be 1-sorted ;

cluster {} T -> empty ;

coherence
{} T is empty ;

end;

registration

let T be empty 1-sorted ;

cluster [#] T -> empty ;

coherence
[#] T is empty ;

end;

registration

let T be non empty 1-sorted ;

cluster [#] T -> non empty ;

coherence
not [#] T is empty ;

end;

registration

let S be non empty 1-sorted ;

cluster non empty for Element of bool the carrier of S;

existence
not for b₁ being Subset of S holds b₁ is empty

proof 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 :: STRUCT_0:def 4
id the carrier of S;

coherence
id the carrier of S is Function of S,S ;

end;

:: deftheorem defines id STRUCT_0:def 4 :
for S being 1-sorted holds id S = id the carrier of S;

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

:: deftheorem defines in STRUCT_0:def 5 :
for S being 1-sorted
for x being object holds
( x in S iff x in the carrier of S );

:: Pointed structures

definition

attr c₁ is strict ;
struct ZeroStr -> 1-sorted ;
aggr ZeroStr(# carrier, ZeroF #) -> ZeroStr ;
sel ZeroF c₁ -> Element of the carrier of c₁;

end;

registration

cluster non empty strict for ZeroStr ;

existence
ex b₁ being ZeroStr st
( b₁ is strict & not b₁ is empty )

proof end;

end;

definition

attr c₁ is strict ;
struct OneStr -> 1-sorted ;
aggr OneStr(# carrier, OneF #) -> OneStr ;
sel OneF c₁ -> Element of the carrier of c₁;

end;

definition

attr c₁ is strict ;
struct ZeroOneStr -> ZeroStr , OneStr ;
aggr ZeroOneStr(# carrier, ZeroF, OneF #) -> ZeroOneStr ;

end;

definition

let S be ZeroStr ;

func 0. S -> Element of S equals :: STRUCT_0:def 6
the ZeroF of S;

coherence
the ZeroF of S is Element of S ;

end;

:: deftheorem defines 0. STRUCT_0:def 6 :
for S being ZeroStr holds 0. S = the ZeroF of S;

definition

let S be OneStr ;

func 1. S -> Element of S equals :: STRUCT_0:def 7
the OneF of S;

coherence
the OneF of S is Element of S ;

end;

:: deftheorem defines 1. STRUCT_0:def 7 :
for S being OneStr holds 1. S = the OneF of S;

definition

let S be ZeroOneStr ;

attr S is degenerated means :Def8: :: STRUCT_0:def 8
0. S = 1. S;

end;

:: deftheorem Def8 defines degenerated STRUCT_0:def 8 :
for S being ZeroOneStr holds
( S is degenerated iff 0. S = 1. S );

definition

let IT be 1-sorted ;

attr IT is trivial means :Def9: :: STRUCT_0:def 9
the carrier of IT is trivial ;

end;

:: deftheorem Def9 defines trivial STRUCT_0:def 9 :
for IT being 1-sorted holds
( IT is trivial iff the carrier of IT is trivial );

registration

cluster empty -> trivial for 1-sorted ;

coherence
for b₁ being 1-sorted st b₁ is empty holds
b₁ is trivial ;

cluster non trivial -> non empty for 1-sorted ;

coherence
for b₁ being 1-sorted st not b₁ is trivial holds
not b₁ is empty ;

end;

definition

let S be 1-sorted ;

redefine attr S is trivial means :Def10: :: STRUCT_0:def 10
for x, y being Element of S holds x = y;

compatibility
( S is trivial iff for x, y being Element of S holds x = y )

proof end;

end;

:: deftheorem Def10 defines trivial STRUCT_0:def 10 :
for S being 1-sorted holds
( S is trivial iff for x, y being Element of S holds x = y );

registration

cluster non degenerated -> non trivial for ZeroOneStr ;

coherence
for b₁ being ZeroOneStr st not b₁ is degenerated holds
not b₁ is trivial ;

end;

registration

cluster strict non empty trivial for 1-sorted ;

existence
ex b₁ being 1-sorted st
( b₁ is trivial & not b₁ is empty & b₁ is strict )

proof end;

cluster strict non trivial for 1-sorted ;

existence
ex b₁ being 1-sorted st
( not b₁ is trivial & b₁ is strict )

proof end;

end;

registration

let S be non trivial 1-sorted ;

cluster the carrier of S -> non trivial ;

coherence
not the carrier of S is trivial by Def9;

end;

registration

let S be trivial 1-sorted ;

cluster the carrier of S -> trivial ;

coherence
the carrier of S is trivial by Def9;

end;

definition

let S be 1-sorted ;

attr S is finite means :Def11: :: STRUCT_0:def 11
the carrier of S is finite ;

end;

:: deftheorem Def11 defines finite STRUCT_0:def 11 :
for S being 1-sorted holds
( S is finite iff the carrier of S is finite );

registration

cluster strict non empty finite for 1-sorted ;

existence
ex b₁ being 1-sorted st
( b₁ is strict & b₁ is finite & not b₁ is empty )

proof end;

end;

registration

let S be finite 1-sorted ;

cluster the carrier of S -> finite ;

coherence
the carrier of S is finite by Def11;

end;

registration

cluster empty -> empty finite for 1-sorted ;

coherence
for b₁ being empty 1-sorted holds b₁ is finite ;

end;

notation

let S be 1-sorted ;
antonym infinite S for finite ;

end;

registration

cluster strict infinite for 1-sorted ;

existence
ex b₁ being 1-sorted st
( b₁ is strict & b₁ is infinite )

proof end;

end;

registration

let S be infinite 1-sorted ;

cluster the carrier of S -> infinite ;

coherence
not the carrier of S is finite by Def11;

end;

registration

cluster infinite -> non empty infinite for 1-sorted ;

coherence
for b₁ being infinite 1-sorted holds not b₁ is empty ;

end;

:: from YELLOW_13, 2007.04.12, A.T.

registration

cluster trivial -> finite for 1-sorted ;

coherence
for b₁ being 1-sorted st b₁ is trivial holds
b₁ is finite ;

end;

registration

cluster infinite -> non trivial for 1-sorted ;

coherence
for b₁ being 1-sorted st b₁ is infinite holds
not b₁ is trivial ;

end;

definition

let S be ZeroStr ;
let x be Element of S;

attr x is zero means :: STRUCT_0:def 12
x = 0. S;

end;

:: deftheorem defines zero STRUCT_0:def 12 :
for S being ZeroStr
for x being Element of S holds
( x is zero iff x = 0. S );

registration

let S be ZeroStr ;

cluster 0. S -> zero ;

coherence
0. S is zero ;

end;

registration

cluster strict non degenerated for ZeroOneStr ;

existence
ex b₁ being ZeroOneStr st
( b₁ is strict & not b₁ is degenerated )

proof end;

end;

registration

let S be non degenerated ZeroOneStr ;

cluster 1. S -> non zero ;

coherence
not 1. S is zero 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
not [#] S is proper ;

end;

definition

attr c₁ is strict ;
struct 2-sorted -> 1-sorted ;
aggr 2-sorted(# carrier, carrier' #) -> 2-sorted ;
sel carrier' c₁ -> set ;

end;

definition

let S be 2-sorted ;

attr S is void means :Def13: :: STRUCT_0:def 13
the carrier' of S is empty ;

end;

:: deftheorem Def13 defines void STRUCT_0:def 13 :
for S being 2-sorted holds
( S is void iff the carrier' of S is empty );

registration

cluster empty strict void for 2-sorted ;

existence
ex b₁ being 2-sorted st
( b₁ is strict & b₁ is empty & b₁ is void )

proof end;

end;

registration

let S be void 2-sorted ;

cluster the carrier' of S -> empty ;

coherence
the carrier' of S is empty by Def13;

end;

registration

cluster non empty strict non void for 2-sorted ;

existence
ex b₁ being 2-sorted st
( b₁ is strict & not b₁ is empty & not b₁ is void )

proof end;

end;

registration

let S be non void 2-sorted ;

cluster the carrier' of S -> non empty ;

coherence
not the carrier' of S is empty by Def13;

end;

:: from BORSUK_1, 2008.07.07, A.T.

definition

let X be 1-sorted ;
let Y be non empty 1-sorted ;
let y be Element of Y;

func X --> y -> Function of X,Y equals :: STRUCT_0:def 14
the carrier of X --> y;

coherence
the carrier of X --> y is Function of X,Y ;

end;

:: deftheorem defines --> STRUCT_0:def 14 :
for X being 1-sorted
for Y being non empty 1-sorted
for y being Element of Y holds X --> y = the carrier of X --> y;

registration

let S be ZeroStr ;

cluster zero for Element of the carrier of S;

existence
ex b₁ being Element of S st b₁ is zero

proof end;

end;

registration

cluster strict non trivial for ZeroStr ;

existence
ex b₁ being ZeroStr st
( b₁ is strict & not b₁ is trivial )

proof end;

end;

registration

let S be non trivial ZeroStr ;

cluster non zero for Element of the carrier of S;

existence
not for b₁ being Element of S holds b₁ is zero

proof end;

end;

:: comp. NDIFF_1, 2008.08.29, A.T.

definition

let X be set ;
let S be ZeroStr ;
let 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;

:: deftheorem defines non-zero STRUCT_0:def 15 :
for X being set
for S being ZeroStr
for R being Relation of X, the carrier of S holds
( R is non-zero iff not 0. S in rng R );

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

coherence
card the carrier of S is Cardinal ;

end;

:: deftheorem defines card STRUCT_0:def 16 :
for S being 1-sorted holds card S = card the carrier of S;

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

coherence
([#] S) \ {(0. S)} is Subset of S ;

end;

:: deftheorem defines NonZero STRUCT_0:def 17 :
for S being ZeroStr holds NonZero S = ([#] S) \ {(0. S)};

theorem :: STRUCT_0:1

for S being non empty ZeroStr
for u being Element of S holds
( u in NonZero S iff not u is zero ) by ZFMISC_1:56;

definition

let V be non empty ZeroStr ;

redefine attr V is trivial means :Def18: :: STRUCT_0:def 18
for u being Element of V holds u = 0. V;

compatibility
( V is trivial iff for u being Element of V holds u = 0. V )

proof end;

end;

:: deftheorem Def18 defines trivial STRUCT_0:def 18 :
for V being non empty ZeroStr holds
( V is trivial iff for u being Element of V holds u = 0. V );

registration

let V be non trivial ZeroStr ;

cluster NonZero V -> non empty ;

coherence
not NonZero V is empty

proof end;

end;

registration

cluster non empty trivial for ZeroStr ;

existence
ex b₁ being ZeroStr st
( b₁ is trivial & not b₁ is empty )

proof end;

end;

registration

let S be non empty trivial ZeroStr ;

cluster NonZero S -> empty ;

coherence
NonZero S is empty

proof end;

end;

registration

let S be non empty 1-sorted ;

cluster non empty trivial for Element of bool the carrier of S;

existence
ex b₁ being Subset of S st
( not b₁ is empty & b₁ is trivial )

proof end;

end;

theorem :: STRUCT_0:2

for F being non degenerated ZeroOneStr holds 1. F in NonZero F

proof end;

:: 2011.03.01, A.T.

registration

let S be finite 1-sorted ;

cluster card S -> natural ;

coherence
card S is natural ;

end;

registration

let S be non empty finite 1-sorted ;

cluster card S -> non zero for Nat;

coherence
for b₁ being Nat st b₁ = card S holds
not b₁ is zero ;

end;

registration

let T be non trivial 1-sorted ;

cluster non trivial for Element of bool the carrier of T;

existence
not for b₁ being Subset of T holds b₁ is trivial

proof end;

end;

:: 2011.04.05, A.T.

theorem :: STRUCT_0:3

for S being ZeroStr holds not 0. S in NonZero S

proof end;

theorem :: STRUCT_0:4

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 ;
let X be 1-sorted ;

attr X is C -element means :Def19: :: STRUCT_0:def 19
the carrier of X is C -element ;

end;

:: deftheorem Def19 defines -element STRUCT_0:def 19 :
for C being set
for X being 1-sorted holds
( X is C -element iff the carrier of X is C -element );

registration

let C be Cardinal;

cluster C -element for 1-sorted ;

existence
ex b₁ being 1-sorted st b₁ is C -element

proof end;

end;

registration

let C be Cardinal;
let X be C -element 1-sorted ;

cluster the carrier of X -> C -element ;

coherence
the carrier of X is C -element by Def19;

end;

registration

cluster empty -> 0 -element for 1-sorted ;

coherence
for b₁ being 1-sorted st b₁ is empty holds
b₁ is 0 -element ;

cluster 0 -element -> empty for 1-sorted ;

coherence
for b₁ being 1-sorted st b₁ is 0 -element holds
b₁ is empty ;

cluster non empty trivial -> 1 -element for 1-sorted ;

coherence
for b₁ being 1-sorted st not b₁ is empty & b₁ is trivial holds
b₁ is 1 -element ;

cluster 1 -element -> non empty trivial for 1-sorted ;

coherence
for b₁ being 1-sorted st b₁ is 1 -element holds
( not b₁ is empty & b₁ is trivial ) ;

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;

:: deftheorem defines feasible STRUCT_0:def 20 :
for S being 2-sorted holds
( S is feasible iff ( the carrier of S is empty implies the carrier' of S is empty ) );

registration

cluster non empty -> feasible for 2-sorted ;

coherence
for b₁ being 2-sorted st not b₁ is empty holds
b₁ is feasible ;

cluster void -> feasible for 2-sorted ;

coherence
for b₁ being 2-sorted st b₁ is void holds
b₁ is feasible ;

cluster empty feasible -> void for 2-sorted ;

coherence
for b₁ being 2-sorted st b₁ is empty & b₁ is feasible holds
b₁ is void ;

cluster non void feasible -> non empty for 2-sorted ;

coherence
for b₁ being 2-sorted st not b₁ is void & b₁ is feasible holds
not b₁ is empty ;

end;

definition

let S be 2-sorted ;

attr S is trivial' means :Def21: :: STRUCT_0:def 21
the carrier' of S is trivial ;

end;

:: deftheorem Def21 defines trivial' STRUCT_0:def 21 :
for S being 2-sorted holds
( S is trivial' iff the carrier' of S is trivial );

registration

cluster non empty trivial strict non void trivial' for 2-sorted ;

existence
ex b₁ being 2-sorted st
( b₁ is strict & not b₁ is empty & not b₁ is void & b₁ is trivial & b₁ is trivial' )

proof end;

end;

registration

let S be trivial' 2-sorted ;

cluster the carrier' of S -> trivial ;

coherence
the carrier' of S is trivial by Def21;

end;

registration

cluster non trivial' for 2-sorted ;

existence
not for b₁ being 2-sorted holds b₁ is trivial'

proof end;

end;

registration

let S be non trivial' 2-sorted ;

cluster the carrier' of S -> non trivial ;

coherence
not the carrier' of S is trivial by Def21;

end;

registration

cluster void -> trivial' for 2-sorted ;

coherence
for b₁ being 2-sorted st b₁ is void holds
b₁ is trivial' ;

cluster non trivial -> non empty for 1-sorted ;

coherence
for b₁ being 1-sorted st not b₁ is trivial holds
not b₁ is empty ;

end;

definition

let x be object ;
let S be 1-sorted ;

func In (x,S) -> Element of S equals :: STRUCT_0:def 22
In (x, the carrier of S);

coherence
In (x, the carrier of S) is Element of S ;

end;

:: deftheorem defines In STRUCT_0:def 22 :
for x being object
for S being 1-sorted holds In (x,S) = In (x, the carrier of S);