:: Miscellaneous Facts about Relation Structure
:: by Agnieszka Julia Marasik
::
:: Received November 8, 1996
:: Copyright (c) 1996-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 RELAT_2, LATTICE3, ORDERS_2, SUBSET_1, EQREL_1, XXREAL_0,
LATTICES, XBOOLE_0, WAYBEL_0, XBOOLEAN;
notations STRUCT_0, LATTICE3, WAYBEL_0, WAYBEL_1, YELLOW_0, ORDERS_2;
constructors LATTICE3, WAYBEL_1;
registrations LATTICE3, YELLOW_0, WAYBEL_1;
begin :: Introduction
theorem :: YELLOW_5:1
for L being reflexive antisymmetric with_suprema RelStr for a being
Element of L holds a "\/" a = a;
theorem :: YELLOW_5:2
for L being reflexive antisymmetric with_infima RelStr for a
being Element of L holds a "/\" a = a;
theorem :: YELLOW_5:3
for L be transitive antisymmetric with_suprema RelStr for a,b,c being
Element of L holds a"\/"b <= c implies a <= c;
theorem :: YELLOW_5:4
for L be transitive antisymmetric with_infima RelStr for a,b,c being
Element of L holds c <= a"/\"b implies c <= a;
theorem :: YELLOW_5:5
for L be antisymmetric transitive with_suprema with_infima RelStr for
a,b,c being Element of L holds a"/\"b <= a"\/"c;
theorem :: YELLOW_5:6
for L be antisymmetric transitive with_infima RelStr for a,b,c be
Element of L holds a <= b implies a"/\"c <= b"/\"c;
theorem :: YELLOW_5:7
for L be antisymmetric transitive with_suprema RelStr for a,b,c
be Element of L holds a <= b implies a"\/"c <= b"\/"c;
theorem :: YELLOW_5:8
for L be sup-Semilattice for a,b be Element of L holds a <= b
implies a "\/" b = b;
theorem :: YELLOW_5:9
for L be sup-Semilattice for a,b,c being Element of L holds a <=
c & b <= c implies a"\/"b <= c;
theorem :: YELLOW_5:10
for L be Semilattice for a,b be Element of L holds b <= a implies a"/\"b = b;
:: Difference in Relation Structure
begin
theorem :: YELLOW_5:11
for L being Boolean LATTICE, x,y being Element of L holds y
is_a_complement_of x iff y = 'not' x;
definition
let L be non empty RelStr, a,b be Element of L;
func a \ b -> Element of L equals
:: YELLOW_5:def 1
a "/\" 'not' b;
end;
definition
let L be non empty RelStr, a, b be Element of L;
func a \+\ b -> Element of L equals
:: YELLOW_5:def 2
(a \ b) "\/" (b \ a);
end;
definition
let L be antisymmetric with_infima with_suprema RelStr, a, b be Element of L;
redefine func a \+\ b;
commutativity;
end;
definition
let L be non empty RelStr, a, b be Element of L;
pred a meets b means
:: YELLOW_5:def 3
a "/\" b <> Bottom L;
end;
notation
let L be non empty RelStr, a, b be Element of L;
antonym a misses b for a meets b;
end;
notation
let L be with_infima antisymmetric RelStr, a, b be Element of L;
antonym a misses b for a meets b;
end;
definition
let L be with_infima antisymmetric RelStr, a, b be Element of L;
redefine pred a meets b;
symmetry;
end;
theorem :: YELLOW_5:12
for L be antisymmetric transitive with_infima with_suprema RelStr for
a,b,c be Element of L holds a <= c implies a \ b <= c;
theorem :: YELLOW_5:13
for L be antisymmetric transitive with_infima with_suprema RelStr for
a,b,c be Element of L holds a <= b implies a \ c <= b \ c;
theorem :: YELLOW_5:14
for L be LATTICE for a,b,c be Element of L holds a \ b <= c & b \ a <=
c implies a \+\ b <= c;
theorem :: YELLOW_5:15
for L be LATTICE for a be Element of L holds a meets a iff a <> Bottom L;
theorem :: YELLOW_5:16
for L be antisymmetric transitive with_infima RelStr st L is
distributive for a,b,c be Element of L holds (a "/\" b) "\/" (a "/\" c) = a
implies a <= b "\/" c;
theorem :: YELLOW_5:17
for L be LATTICE st L is distributive for a,b,c be Element of L
holds a"\/"(b"/\"c) = (a"\/"b) "/\" (a"\/"c);
theorem :: YELLOW_5:18
for L be LATTICE st L is distributive for a,b,c be Element of L holds
(a "\/" b) \ c = (a \ c) "\/" (b \ c);
:: Lower-bound in Relation Structure
begin
theorem :: YELLOW_5:19
for L be lower-bounded non empty antisymmetric RelStr for a be
Element of L holds a <= Bottom L implies a = Bottom L;
theorem :: YELLOW_5:20
for L be lower-bounded Semilattice for a,b,c be Element of L holds a
<= b & a <= c & b"/\"c = Bottom L implies a = Bottom L;
theorem :: YELLOW_5:21
for L be lower-bounded antisymmetric with_suprema RelStr for a,b be
Element of L holds a"\/"b = Bottom L implies a = Bottom L & b = Bottom L;
theorem :: YELLOW_5:22
for L be lower-bounded antisymmetric transitive with_infima RelStr for
a,b,c be Element of L holds a <= b & b"/\"c = Bottom L implies a"/\"c = Bottom
L;
theorem :: YELLOW_5:23
for L be lower-bounded Semilattice for a be Element of L holds Bottom
L \ a = Bottom L;
theorem :: YELLOW_5:24
for L be lower-bounded antisymmetric transitive with_infima RelStr for
a,b,c be Element of L holds a meets b & b <= c implies a meets c;
theorem :: YELLOW_5:25
for L be lower-bounded with_infima antisymmetric RelStr for a be
Element of L holds a"/\"Bottom L = Bottom L;
theorem :: YELLOW_5:26
for L be lower-bounded antisymmetric transitive with_infima
with_suprema RelStr for a,b,c be Element of L holds a meets b"/\"c implies a
meets b;
theorem :: YELLOW_5:27
for L be lower-bounded antisymmetric transitive with_infima
with_suprema RelStr for a,b,c be Element of L holds a meets b\c implies a meets
b;
theorem :: YELLOW_5:28
for L be lower-bounded antisymmetric transitive with_infima RelStr for
a be Element of L holds a misses Bottom L;
theorem :: YELLOW_5:29
for L be lower-bounded antisymmetric transitive with_infima RelStr for
a,b,c be Element of L holds a misses c & b <= c implies a misses b;
theorem :: YELLOW_5:30
for L be lower-bounded antisymmetric transitive with_infima RelStr for
a,b,c be Element of L holds a misses b or a misses c implies a misses b"/\"c;
theorem :: YELLOW_5:31
for L be lower-bounded LATTICE for a,b,c be Element of L holds a <= b
& a <= c & b misses c implies a = Bottom L;
theorem :: YELLOW_5:32
for L be lower-bounded antisymmetric transitive with_infima RelStr for
a,b,c be Element of L holds a misses b implies (a"/\"c) misses (b"/\"c);
:: Boolean Lattice
begin
reserve L for Boolean non empty RelStr;
reserve a,b,c,d for Element of L;
theorem :: YELLOW_5:33
(a"/\"b) "\/" (b"/\"c) "\/" (c"/\"a) = (a"\/"b) "/\" (b"\/"c) "/\" (c
"\/" a );
theorem :: YELLOW_5:34
a"/\"'not' a = Bottom L & a"\/"'not' a = Top L;
theorem :: YELLOW_5:35
a \ b <= c implies a <= b"\/"c;
theorem :: YELLOW_5:36
'not' (a"\/"b) = 'not' a"/\" 'not' b & 'not' (a"/\"b) = 'not' a "\/" 'not' b;
theorem :: YELLOW_5:37
a <= b implies 'not' b <= 'not' a;
theorem :: YELLOW_5:38
a <= b implies c\b <= c\a;
theorem :: YELLOW_5:39
a <= b & c <= d implies a\d <= b\c;
theorem :: YELLOW_5:40
a <= b"\/"c implies a\b <= c & a\c <= b;
theorem :: YELLOW_5:41
'not' a <= 'not' (a"/\"b) & 'not' b <= 'not' (a"/\"b);
theorem :: YELLOW_5:42
'not' (a"\/"b) <= 'not' a & 'not' (a"\/"b) <= 'not' b;
theorem :: YELLOW_5:43
a <= b\a implies a = Bottom L;
theorem :: YELLOW_5:44
a <= b implies b = a "\/" (b\a);
theorem :: YELLOW_5:45
a\b = Bottom L iff a <= b;
theorem :: YELLOW_5:46
a <= b"\/"c & a"/\"c = Bottom L implies a <= b;
theorem :: YELLOW_5:47
a"\/"b = (a\b)"\/"b;
theorem :: YELLOW_5:48
a\(a"\/"b) = Bottom L;
theorem :: YELLOW_5:49
a\a"/\"b = a\b;
theorem :: YELLOW_5:50
(a\b)"/\"b = Bottom L;
theorem :: YELLOW_5:51
a"\/"(b\a) = a"\/"b;
theorem :: YELLOW_5:52
(a"/\"b)"\/"(a\b) = a;
theorem :: YELLOW_5:53
a\(b\c)= (a\b)"\/"(a"/\"c);
theorem :: YELLOW_5:54
a\(a\b) = a"/\"b;
theorem :: YELLOW_5:55
(a"\/"b)\b = a\b;
theorem :: YELLOW_5:56
a"/\"b = Bottom L iff a\b = a;
theorem :: YELLOW_5:57
a\(b"\/"c) = (a\b)"/\"(a\c);
theorem :: YELLOW_5:58
a\(b"/\"c) = (a\b)"\/"(a\c);
theorem :: YELLOW_5:59
a"/\"(b\c) = a"/\"b \ a"/\"c;
theorem :: YELLOW_5:60
(a"\/"b)\(a"/\"b) = (a\b)"\/"(b\a);
theorem :: YELLOW_5:61
(a\b)\c = a\(b"\/"c);
theorem :: YELLOW_5:62
'not' (Bottom L) = Top L;
theorem :: YELLOW_5:63
'not' (Top L) = Bottom L;
theorem :: YELLOW_5:64
a\a = Bottom L;
theorem :: YELLOW_5:65
a \ Bottom L = a;
theorem :: YELLOW_5:66
'not' (a\b) = 'not' a"\/"b;
theorem :: YELLOW_5:67
a"/\"b misses a\b;
theorem :: YELLOW_5:68
(a\b) misses b;
theorem :: YELLOW_5:69
a misses b implies (a"\/"b)\b = a;