:: Group and Field Definitions
:: by J\'ozef Bia{\l}as
::
:: Received October 27, 1989
:: Copyright (c) 1990 Association of Mizar Users

begin

theorem Th1: :: REALSET1:1

for X, x being set
for F being Function of [:X,X:],X st x in [:X,X:] holds
F . x in X

proof end;

definition

let X be set ;
let F be BinOp of X;
let A be Subset of X;
pred F is_in A means :: REALSET1:def 1
for x being set st x in [:A,A:] holds
F . x in A;

end;

:: deftheorem defines is_in REALSET1:def 1 :
for X being set
for F being BinOp of X
for A being Subset of X holds
( F is_in A iff for x being set st x in [:A,A:] holds
F . x in A );

definition

let X be set ;
let F be BinOp of X;
mode Preserv of F -> Subset of X means :Def2: :: REALSET1:def 2
for x being set st x in [:it,it:] holds
F . x in it;
existence
ex b₁ being Subset of X st
for x being set st x in [:b₁,b₁:] holds
F . x in b₁

proof end;

end;

:: deftheorem Def2 defines Preserv REALSET1:def 2 :
for X being set
for F being BinOp of X
for b₃ being Subset of X holds
( b₃ is Preserv of F iff for x being set st x in [:b₃,b₃:] holds
F . x in b₃ );

definition

let R be Relation;
let A be set ;
func R || A -> set equals :: REALSET1:def 3
R | [:A,A:];
coherence
R | [:A,A:] is set ;

end;

:: deftheorem defines || REALSET1:def 3 :
for R being Relation
for A being set holds R || A = R | [:A,A:];

registration

let R be Relation;
let A be set ;
cluster R || A -> Relation-like ;
coherence
R || A is Relation-like ;

end;

registration

let R be Function;
let A be set ;
cluster R || A -> Function-like ;
coherence
R || A is Function-like ;

end;

theorem :: REALSET1:2

canceled;

theorem Th3: :: REALSET1:3

for X being set
for F being BinOp of X
for A being Preserv of F holds F || A is BinOp of A

proof end;

definition

let X be set ;
let F be BinOp of X;
let A be Preserv of F;
:: original: ||
redefine func F || A -> BinOp of A;
coherence
F || A is BinOp of A by Th3;

end;

definition

let IT be set ;
redefine attr IT is trivial means :Def4: :: REALSET1:def 4
( IT is empty or ex x being set st IT = {x} );
compatibility
( IT is trivial iff ( IT is empty or ex x being set st IT = {x} ) )

proof end;

end;

:: deftheorem Def4 defines trivial REALSET1:def 4 :
for IT being set holds
( IT is trivial iff ( IT is empty or ex x being set st IT = {x} ) );

registration

cluster non empty trivial set ;
existence
ex b₁ being set st
( b₁ is trivial & not b₁ is empty )

proof end;

cluster non empty non trivial set ;
existence
ex b₁ being set st
( not b₁ is trivial & not b₁ is empty )

proof end;

cluster non trivial -> non empty set ;
coherence
for b₁ being set st not b₁ is trivial holds
not b₁ is empty ;

end;

theorem Th4: :: REALSET1:4

for X being non empty set holds
( not X is trivial iff for x being set holds X \ {x} is non empty set )

proof end;

theorem :: REALSET1:5

ex A being non empty set st
for z being Element of A holds A \ {z} is non empty set

proof end;

theorem Th6: :: REALSET1:6

for X being non empty set st ( for x being Element of X holds X \ {x} is non empty set ) holds
not X is trivial

proof end;

theorem :: REALSET1:7

for A being non empty set st ( for x being Element of A holds A \ {x} is non empty set ) holds
A is non trivial set by Th6;

definition

let X be non trivial set ;
let F be BinOp of X;
let x be Element of X;
pred F is_Bin_Op_Preserv x means :: REALSET1:def 5
( X \ {x} is Preserv of F & (F || X) \ {x} is BinOp of (X \ {x}) );
correctness
;

end;

:: deftheorem defines is_Bin_Op_Preserv REALSET1:def 5 :
for X being non trivial set
for F being BinOp of X
for x being Element of X holds
( F is_Bin_Op_Preserv x iff ( X \ {x} is Preserv of F & (F || X) \ {x} is BinOp of (X \ {x}) ) );

theorem Th8: :: REALSET1:8

for X being set
for A being Subset of X ex F being BinOp of X st
for x being set st x in [:A,A:] holds
F . x in A

proof end;

definition

let X be set ;
let A be Subset of X;
mode Presv of X,A -> BinOp of X means :Def6: :: REALSET1:def 6
for x being set st x in [:A,A:] holds
it . x in A;
existence
ex b₁ being BinOp of X st
for x being set st x in [:A,A:] holds
b₁ . x in A by Th8;

end;

:: deftheorem Def6 defines Presv REALSET1:def 6 :
for X being set
for A being Subset of X
for b₃ being BinOp of X holds
( b₃ is Presv of X,A iff for x being set st x in [:A,A:] holds
b₃ . x in A );

theorem Th9: :: REALSET1:9

for X being set
for A being Subset of X
for F being Presv of X,A holds F || A is BinOp of A

proof end;

definition

let X be set ;
let A be Subset of X;
let F be Presv of X,A;
func F ||| A -> BinOp of A equals :: REALSET1:def 7
F || A;
coherence
F || A is BinOp of A by Th9;

end;

:: deftheorem defines ||| REALSET1:def 7 :
for X being set
for A being Subset of X
for F being Presv of X,A holds F ||| A = F || A;

theorem :: REALSET1:10

canceled;

definition

let A be set ;
let x be Element of A;
mode DnT of x,A -> BinOp of A means :Def8: :: REALSET1:def 8
for y being set st y in [:(A \ {x}),(A \ {x}):] holds
it . y in A \ {x};
existence
ex b₁ being BinOp of A st
for y being set st y in [:(A \ {x}),(A \ {x}):] holds
b₁ . y in A \ {x} by Th8;

end;

:: deftheorem Def8 defines DnT REALSET1:def 8 :
for A being set
for x being Element of A
for b₃ being BinOp of A holds
( b₃ is DnT of x,A iff for y being set st y in [:(A \ {x}),(A \ {x}):] holds
b₃ . y in A \ {x} );

theorem Th11: :: REALSET1:11

for A being non trivial set
for x being Element of A
for F being DnT of x,A holds F || (A \ {x}) is BinOp of (A \ {x})

proof end;

definition

let A be non trivial set ;
let x be Element of A;
let F be DnT of x,A;
func F ! (A,x) -> BinOp of (A \ {x}) equals :: REALSET1:def 9
F || (A \ {x});
coherence
F || (A \ {x}) is BinOp of (A \ {x}) by Th11;

end;

:: deftheorem defines ! REALSET1:def 9 :
for A being non trivial set
for x being Element of A
for F being DnT of x,A holds F ! (A,x) = F || (A \ {x});

registration

let F be non empty set ;
cluster non empty trivial Element of bool F;
existence
ex b₁ being Subset of F st
( b₁ is trivial & not b₁ is empty )

proof end;

end;

definition

let F be non empty set ;
mode OnePoint of F is non empty trivial Subset of F;

end;

Lm1: for F being non trivial set
for A being OnePoint of F ex x being Element of F st A = {x}

proof end;

theorem Th12: :: REALSET1:12

for F being non trivial set
for A being OnePoint of F holds F \ A is non empty set

proof end;

registration

let F be non trivial set ;
let A be OnePoint of F;
cluster F \ A -> non empty ;
coherence
not F \ A is empty by Th12;

end;

begin

theorem :: REALSET1:13

for A being finite set holds
( A is trivial iff card A < 2 )

proof end;

theorem Th14: :: REALSET1:14

for A being set holds
( not A is trivial iff ex a1, a2 being set st
( a1 in A & a2 in A & a1 <> a2 ) )

proof end;

theorem :: REALSET1:15

for D being set
for A being Subset of D holds
( not A is trivial iff ex d1, d2 being Element of D st
( d1 in A & d2 in A & d1 <> d2 ) )

proof end;

theorem :: REALSET1:16

for F being non trivial set
for A being OnePoint of F ex x being Element of F st A = {x} by Lm1;

begin

registration

let x, y be set ;
cluster x .--> y -> trivial ;
coherence
x .--> y is trivial

proof end;

end;

registration

cluster empty -> trivial set ;
coherence
for b₁ being set st b₁ is empty holds
b₁ is trivial ;

end;

registration

cluster trivial -> finite set ;
coherence
for b₁ being set st b₁ is trivial holds
b₁ is finite

proof end;

end;

registration

cluster infinite -> non trivial set ;
coherence
for b₁ being set st not b₁ is finite holds
not b₁ is trivial ;

end;

theorem :: REALSET1:17

for x being set
for X being trivial set st x in X holds
X = {x}

proof end;

registration

let f be non trivial Function;
cluster proj1 f -> non trivial ;
coherence
not dom f is trivial

proof end;

end;