:: Boolean Properties of Sets - Requirements
:: by Library Committee
::
:: Received April 30, 2002
:: Copyright (c) 2002-2021 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, TARSKI;
notations TARSKI, XBOOLE_0;
constructors TARSKI, XBOOLE_0;
definitions XBOOLE_0, TARSKI;
equalities XBOOLE_0;
expansions TARSKI;
theorems XBOOLE_0, TARSKI;
begin
:: This file contains statements which are obvious for Mizar checker if
:: "requirements BOOLE" is included in the environment description
:: of an article. They are published for testing purposes only.
:: Users should use appropriate requirements instead of referencing
:: to these theorems.
:: Statements which cannot be expressed in Mizar language are commented out.
theorem
for X being set holds X \/ {} = X
proof
let X be set;
thus X \/ {} c= X
proof
let x be object;
assume x in X \/ {};
then x in X or x in {} by XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 1;
end;
let x be object;
assume x in X;
hence thesis by XBOOLE_0:def 3;
end;
theorem
for X being set holds X /\ {} = {}
proof
let X be set;
thus X /\ {} c= {}
by XBOOLE_0:def 4;
let x be object;
assume x in {};
hence thesis by XBOOLE_0:def 1;
end;
theorem
for X being set holds X \ {} = X
proof
let X be set;
thus X \ {} c= X
by XBOOLE_0:def 5;
let x be object;
A1: not x in {} by XBOOLE_0:def 1;
assume x in X;
hence thesis by A1,XBOOLE_0:def 5;
end;
theorem
for X being set holds {} \ X = {}
proof
let X be set;
thus {} \ X c= {}
by XBOOLE_0:def 5;
let x be object;
assume x in {};
hence thesis by XBOOLE_0:def 1;
end;
theorem
for X being set holds X \+\ {} = X
proof
let X be set;
thus X \+\ {} c= X
proof
let x be object;
assume x in X \+\ {};
then
A1: x in X \ {} or x in {} \ X by XBOOLE_0:def 3;
per cases by A1,XBOOLE_0:def 5;
suppose
x in X & not x in {};
hence thesis;
end;
suppose
x in {} & not x in X;
hence thesis by XBOOLE_0:def 1;
end;
end;
let x be object;
A2: not x in {} by XBOOLE_0:def 1;
assume x in X;
then x in X \ {} by A2,XBOOLE_0:def 5;
hence thesis by XBOOLE_0:def 3;
end;
reserve x,X for set;
Lm1: X is empty implies X = {}
proof
assume not ex x being object st x in X;
then for x being object holds x in {} iff x in X by XBOOLE_0:def 1;
hence thesis by TARSKI:2;
end;
theorem
for X being set st X is empty holds X = {} by Lm1;
theorem
for x, X being set st x in X holds X is non empty by XBOOLE_0:def 1;
theorem
for X, Y being set st X is empty & X <> Y holds Y is non empty
proof
let X, Y be set;
assume that
A1: X is empty and
A2: X <> Y;
X = {} by A1,Lm1;
hence thesis by A2,Lm1;
end;
::theorem :: equality of 0 and {} is assumed
:: 0 is empty;
::theorem
:: for X being set holds
:: numeral(X) & X <> 0 implies X is non empty;