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