:: by Library Committee

::

:: Received January 6, 1995

:: Copyright (c) 1995-2012 Association of Mizar Users

begin

definition

attr c_{1} is strict ;

struct 1-sorted -> ;

aggr 1-sorted(# carrier #) -> 1-sorted ;

sel carrier c_{1} -> set ;

end;
struct 1-sorted -> ;

aggr 1-sorted(# carrier #) -> 1-sorted ;

sel carrier c

definition
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 );

for S being 1-sorted holds

( S is empty iff the carrier of S is empty );

registration
end;

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

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

definition
end;

:: from PRE_TOPC, 2006.12.02, AT

definition

let T be 1-sorted ;

coherence

{} is Subset of T

the carrier of T is Subset of T

end;
coherence

{} is Subset of T

proof end;

coherence the carrier of T is Subset of T

proof end;

registration
end;

registration

let S be non empty 1-sorted ;

existence

not for b_{1} being Subset of S holds b_{1} is empty

end;
existence

not for b

proof end;

::Moved from TOPREAL1 on 2005.09.22

::Moved from YELLOW18, AK, 21.02.2006

::Moved from GRCAT_1, AK, 16.01.2007

::Moved from NORMSP_1, AK, 14.02.2007

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

definition
end;

::Moved from RLVECT_1, 2007.02.19, A.T.

definition
end;

:: deftheorem defines in STRUCT_0:def 5 :

for S being 1-sorted

for x being set holds

( x in S iff x in the carrier of S );

for S being 1-sorted

for x being set holds

( x in S iff x in the carrier of S );

:: Pointed structures

definition

attr c_{1} is strict ;

struct ZeroStr -> 1-sorted ;

aggr ZeroStr(# carrier, ZeroF #) -> ZeroStr ;

sel ZeroF c_{1} -> Element of the carrier of c_{1};

end;
struct ZeroStr -> 1-sorted ;

aggr ZeroStr(# carrier, ZeroF #) -> ZeroStr ;

sel ZeroF c

registration
end;

definition

attr c_{1} is strict ;

struct OneStr -> 1-sorted ;

aggr OneStr(# carrier, OneF #) -> OneStr ;

sel OneF c_{1} -> Element of the carrier of c_{1};

end;
struct OneStr -> 1-sorted ;

aggr OneStr(# carrier, OneF #) -> OneStr ;

sel OneF c

definition

attr c_{1} is strict ;

struct ZeroOneStr -> ZeroStr , OneStr ;

aggr ZeroOneStr(# carrier, ZeroF, OneF #) -> ZeroOneStr ;

end;
struct ZeroOneStr -> ZeroStr , OneStr ;

aggr ZeroOneStr(# carrier, ZeroF, OneF #) -> ZeroOneStr ;

definition
end;

:: deftheorem Def8 defines degenerated STRUCT_0:def 8 :

for S being ZeroOneStr holds

( S is degenerated iff 0. S = 1. S );

for S being ZeroOneStr holds

( S is degenerated iff 0. S = 1. S );

:: deftheorem Def9 defines trivial STRUCT_0:def 9 :

for IT being 1-sorted holds

( IT is trivial iff the carrier of IT is trivial );

for IT being 1-sorted holds

( IT is trivial iff the carrier of IT is trivial );

registration

coherence

for b_{1} being 1-sorted st b_{1} is empty holds

b_{1} is trivial

for b_{1} being 1-sorted st not b_{1} is trivial holds

not b_{1} is empty
;

end;
for b

b

proof end;

coherence for b

not b

definition

let S be 1-sorted ;

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

end;
redefine attr S is trivial means :Def10: :: STRUCT_0:def 10

for x, y being Element of S holds x = y;

compatibility for x, y being Element of S holds x = y;

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

proof 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 );

for S being 1-sorted holds

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

registration

coherence

for b_{1} being ZeroOneStr st not b_{1} is degenerated holds

not b_{1} is trivial

end;
for b

not b

proof end;

registration

existence

ex b_{1} being 1-sorted st

( b_{1} is trivial & not b_{1} is empty & b_{1} is strict )

ex b_{1} being 1-sorted st

( not b_{1} is trivial & b_{1} is strict )

end;
ex b

( b

proof end;

existence ex b

( not b

proof end;

registration
end;

begin

definition
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 );

for S being 1-sorted holds

( S is finite iff the carrier of S is finite );

registration

existence

ex b_{1} being 1-sorted st

( b_{1} is strict & b_{1} is finite & not b_{1} is empty )

end;
ex b

( b

proof end;

registration
end;

:: from YELLOW_13, 2007.04.12, A.T.

registration
end;

registration
end;

definition
end;

:: deftheorem Def12 defines zero STRUCT_0:def 12 :

for S being ZeroStr

for x being Element of S holds

( x is zero iff x = 0. S );

for S being ZeroStr

for x being Element of S holds

( x is zero iff x = 0. S );

registration
end;

:: from RING_1, 2008.06.19, A.T. (needed in TEX_2)

registration
end;

begin

definition

attr c_{1} is strict ;

struct 2-sorted -> 1-sorted ;

aggr 2-sorted(# carrier, carrier' #) -> 2-sorted ;

sel carrier' c_{1} -> set ;

end;
struct 2-sorted -> 1-sorted ;

aggr 2-sorted(# carrier, carrier' #) -> 2-sorted ;

sel carrier' c

definition
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 );

for S being 2-sorted holds

( S is void iff the carrier' of S is empty );

registration

existence

ex b_{1} being 2-sorted st

( b_{1} is strict & b_{1} is empty & b_{1} is void )

end;
ex b

( b

proof end;

registration

existence

ex b_{1} being 2-sorted st

( b_{1} is strict & not b_{1} is empty & not b_{1} is void )

end;
ex b

( b

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

coherence

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

end;
let Y be non empty 1-sorted ;

let y be Element of Y;

coherence

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

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

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

registration
end;

registration

let S be non trivial ZeroStr ;

existence

not for b_{1} being Element of S holds b_{1} is zero

end;
existence

not for b

proof end;

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

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

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.

:: deftheorem defines card STRUCT_0:def 16 :

for S being 1-sorted holds card S = card the carrier of S;

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;
mode UnOp of S is UnOp of the carrier of S;

mode BinOp of S is BinOp of the carrier of S;

:: 2009.01.24, A.T.

:: deftheorem defines NonZero STRUCT_0:def 17 :

for S being ZeroStr holds NonZero S = ([#] S) \ {(0. S)};

for S being ZeroStr holds NonZero S = ([#] S) \ {(0. S)};

definition

let V be non empty ZeroStr ;

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

end;
redefine attr V is trivial means :Def18: :: STRUCT_0:def 18

for u being Element of V holds u = 0. V;

compatibility for u being Element of V holds u = 0. V;

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

proof 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 );

for V being non empty ZeroStr holds

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

registration
end;

registration

let S be non empty 1-sorted ;

existence

ex b_{1} being Subset of S st

( not b_{1} is empty & b_{1} is trivial )

end;
existence

ex b

( not b

proof end;

:: 2011.03.01, A.T.

registration
end;

registration

let S be non empty finite 1-sorted ;

coherence

for b_{1} being Nat st b_{1} = card S holds

not b_{1} is empty
;

end;
coherence

for b

not b

registration

let T be non trivial 1-sorted ;

existence

not for b_{1} being Subset of T holds b_{1} is trivial

end;
existence

not for b

proof end;

:: 2011.04.05, A.T.

theorem :: STRUCT_0:4

:: 2011.05.02, A.T.

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

for C being set

for X being 1-sorted holds

( X is C -element iff the carrier of X is C -element );

registration
end;

registration
end;

registration

coherence

for b_{1} being 1-sorted st b_{1} is empty holds

b_{1} is 0 -element

for b_{1} being 1-sorted st b_{1} is 0 -element holds

b_{1} is empty

for b_{1} being 1-sorted st not b_{1} is empty & b_{1} is trivial holds

b_{1} is 1 -element

for b_{1} being 1-sorted st b_{1} is 1 -element holds

( not b_{1} is empty & b_{1} is trivial )

end;
for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;

coherence for b

( not b

proof end;

:: Feasibility, 2011.11.15, A.T.

:: deftheorem Def20 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 ) );

for S being 2-sorted holds

( S is feasible iff ( the carrier of S is empty implies the carrier' of S is empty ) );

registration

coherence

for b_{1} being 2-sorted st not b_{1} is empty holds

b_{1} is feasible

for b_{1} being 2-sorted st b_{1} is void holds

b_{1} is feasible

for b_{1} being 2-sorted st b_{1} is empty & b_{1} is feasible holds

b_{1} is void

for b_{1} being 2-sorted st not b_{1} is void & b_{1} is feasible holds

not b_{1} is empty
;

end;
for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;

coherence for b

not b

:: deftheorem Def21 defines trivial' STRUCT_0:def 21 :

for S being 2-sorted holds

( S is trivial' iff the carrier' of S is trivial );

for S being 2-sorted holds

( S is trivial' iff the carrier' of S is trivial );

registration

existence

ex b_{1} being 2-sorted st

( b_{1} is strict & not b_{1} is empty & not b_{1} is void & b_{1} is trivial & b_{1} is trivial' )

end;
ex b

( b

proof end;

registration
end;

registration

coherence

for b_{1} being 2-sorted st b_{1} is void holds

b_{1} is trivial'

for b_{1} being 1-sorted st not b_{1} is trivial holds

not b_{1} is empty
;

end;
for b

b

proof end;

coherence for b

not b

:: Moved from ALG_1, GROUP_6, PRE_TOPC, POLYNOM1