:: Group and Field Definitions
:: by J\'ozef Bia{\l}as
::
:: Received October 27, 1989
:: Copyright (c) 1990-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 FUNCT_1, ZFMISC_1, XBOOLE_0, RELAT_1, TARSKI, BINOP_1, SUBSET_1,
MCART_1, REALSET1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2,
BINOP_1, DOMAIN_1, FUNCOP_1, FUNCT_3;
constructors BINOP_1, DOMAIN_1, FUNCT_3, FUNCOP_1, RELSET_1, SETFAM_1;
registrations XBOOLE_0, FUNCT_1, RELSET_1, ZFMISC_1, FUNCT_2;
requirements SUBSET, BOOLE;
begin
theorem :: REALSET1:1
for X,x being set holds for F being Function of [:X,X:],X holds x
in [:X,X:] implies F.x in X;
definition
let X be set;
let F be BinOp of X;
mode Preserv of F -> Subset of X means
:: REALSET1:def 1
for x being set holds x in [: it,it:] implies F.x in it;
end;
definition
let R be Relation;
let A be set;
func R||A -> set equals
:: REALSET1:def 2
R | [:A,A:];
end;
registration
let R be Relation;
let A be set;
cluster R||A -> Relation-like;
end;
registration
let R be Function;
let A be set;
cluster R||A -> Function-like;
end;
theorem :: REALSET1:2
for X being set, F being BinOp of X, A being Preserv of F holds F
||A is BinOp of A;
definition
let X be set;
let F be BinOp of X;
let A be Preserv of F;
redefine func F||A -> BinOp of A;
end;
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 3
X\{x} is Preserv of F & F||X\{x} is BinOp of X\{x};
end;
::$CT 2
theorem :: REALSET1:5
for X being set holds for A being Subset of X holds ex F being
BinOp of X st for x being set holds x in [:A,A:] implies F.x in A;
definition
let X be set;
let A be Subset of X;
mode Presv of X,A -> BinOp of X means
:: REALSET1:def 4
for x being set holds x in [:A, A:] implies it.x in A;
end;
theorem :: REALSET1:6
for X being set, A being Subset of X, F being Presv of X,A holds
F||A is BinOp of A;
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 5
F||A;
end;
definition
let A be set;
let x be Element of A;
mode DnT of x,A -> BinOp of A means
:: REALSET1:def 6
for y being set holds y in [:A\{x },A\{x}:] implies it.y in A\{x};
end;
theorem :: REALSET1:7
for A being non trivial set holds for x being Element of A holds
for F being DnT of x,A holds F||(A\{x}) is BinOp of A\{x};
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 7
F||(A\{x});
end;