:: Definitions and Properties of the Join and Meet of Subsets
:: by Artur Korni{\l}owicz
::
:: Received September 25, 1996
:: Copyright (c) 1996 Association of Mizar Users
theorem Th1: :: YELLOW_4:1
theorem Th2: :: YELLOW_4:2
:: deftheorem Def1 defines is_finer_than YELLOW_4:def 1 :
:: deftheorem Def2 defines is_coarser_than YELLOW_4:def 2 :
theorem :: YELLOW_4:3
theorem :: YELLOW_4:4
theorem :: YELLOW_4:5
theorem :: YELLOW_4:6
theorem :: YELLOW_4:7
theorem :: YELLOW_4:8
:: deftheorem defines "\/" YELLOW_4:def 3 :
theorem :: YELLOW_4:9
theorem :: YELLOW_4:10
theorem :: YELLOW_4:11
theorem :: YELLOW_4:12
theorem :: YELLOW_4:13
theorem :: YELLOW_4:14
theorem Th15: :: YELLOW_4:15
theorem :: YELLOW_4:16
theorem :: YELLOW_4:17
theorem :: YELLOW_4:18
Lm2:
now
let L be non
empty RelStr ;
:: thesis: for x, y, z being Element of L holds { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } = {(x "\/" y),(x "\/" z)}let x,
y,
z be
Element of
L;
:: thesis: { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } = {(x "\/" y),(x "\/" z)}thus
{ (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } = {(x "\/" y),(x "\/" z)}
:: thesis: verum
proof
thus
{ (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } c= {(x "\/" y),(x "\/" z)}
:: according to XBOOLE_0:def 10 :: thesis: {(x "\/" y),(x "\/" z)} c= { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) }
proof
let q be
set ;
:: according to TARSKI:def 3 :: thesis: ( not q in { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } or q in {(x "\/" y),(x "\/" z)} )
assume
q in { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) }
;
:: thesis: q in {(x "\/" y),(x "\/" z)}
then consider u,
v being
Element of
L such that A1:
q = u "\/" v
and A2:
(
u in {x} &
v in {y,z} )
;
(
u = x & (
v = y or
v = z ) )
by A2, TARSKI:def 1, TARSKI:def 2;
hence
q in {(x "\/" y),(x "\/" z)}
by A1, TARSKI:def 2;
:: thesis: verum
end;
let q be
set ;
:: according to TARSKI:def 3 :: thesis: ( not q in {(x "\/" y),(x "\/" z)} or q in { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } )
assume
q in {(x "\/" y),(x "\/" z)}
;
:: thesis: q in { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) }
then A3:
(
q = x "\/" y or
q = x "\/" z )
by TARSKI:def 2;
(
x in {x} &
y in {y,z} &
z in {y,z} )
by TARSKI:def 1, TARSKI:def 2;
hence
q in { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) }
by A3;
:: thesis: verum
end;
end;
theorem :: YELLOW_4:19
theorem :: YELLOW_4:20
theorem :: YELLOW_4:21
theorem :: YELLOW_4:22
theorem :: YELLOW_4:23
theorem :: YELLOW_4:24
theorem Th25: :: YELLOW_4:25
theorem :: YELLOW_4:26
theorem Th27: :: YELLOW_4:27
theorem :: YELLOW_4:28
theorem Th29: :: YELLOW_4:29
theorem :: YELLOW_4:30
theorem :: YELLOW_4:31
theorem Th32: :: YELLOW_4:32
theorem :: YELLOW_4:33
theorem Th34: :: YELLOW_4:34
theorem :: YELLOW_4:35
:: deftheorem defines "/\" YELLOW_4:def 4 :
theorem :: YELLOW_4:36
theorem :: YELLOW_4:37
theorem :: YELLOW_4:38
theorem :: YELLOW_4:39
theorem :: YELLOW_4:40
theorem :: YELLOW_4:41
theorem Th42: :: YELLOW_4:42
theorem :: YELLOW_4:43
theorem :: YELLOW_4:44
theorem :: YELLOW_4:45
Lm4:
now
let L be non
empty RelStr ;
:: thesis: for x, y, z being Element of L holds { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } = {(x "/\" y),(x "/\" z)}let x,
y,
z be
Element of
L;
:: thesis: { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } = {(x "/\" y),(x "/\" z)}thus
{ (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } = {(x "/\" y),(x "/\" z)}
:: thesis: verum
proof
thus
{ (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } c= {(x "/\" y),(x "/\" z)}
:: according to XBOOLE_0:def 10 :: thesis: {(x "/\" y),(x "/\" z)} c= { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) }
proof
let q be
set ;
:: according to TARSKI:def 3 :: thesis: ( not q in { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } or q in {(x "/\" y),(x "/\" z)} )
assume
q in { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) }
;
:: thesis: q in {(x "/\" y),(x "/\" z)}
then consider u,
v being
Element of
L such that A1:
q = u "/\" v
and A2:
(
u in {x} &
v in {y,z} )
;
(
u = x & (
v = y or
v = z ) )
by A2, TARSKI:def 1, TARSKI:def 2;
hence
q in {(x "/\" y),(x "/\" z)}
by A1, TARSKI:def 2;
:: thesis: verum
end;
let q be
set ;
:: according to TARSKI:def 3 :: thesis: ( not q in {(x "/\" y),(x "/\" z)} or q in { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } )
assume
q in {(x "/\" y),(x "/\" z)}
;
:: thesis: q in { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) }
then A3:
(
q = x "/\" y or
q = x "/\" z )
by TARSKI:def 2;
(
x in {x} &
y in {y,z} &
z in {y,z} )
by TARSKI:def 1, TARSKI:def 2;
hence
q in { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) }
by A3;
:: thesis: verum
end;
end;
theorem :: YELLOW_4:46
theorem :: YELLOW_4:47
theorem :: YELLOW_4:48
theorem Th49: :: YELLOW_4:49
theorem Th50: :: YELLOW_4:50
theorem :: YELLOW_4:51
theorem :: YELLOW_4:52
theorem :: YELLOW_4:53
theorem Th54: :: YELLOW_4:54
theorem Th55: :: YELLOW_4:55
theorem :: YELLOW_4:56
theorem :: YELLOW_4:57
theorem :: YELLOW_4:58
theorem :: YELLOW_4:59
theorem :: YELLOW_4:60
theorem Th61: :: YELLOW_4:61
theorem :: YELLOW_4:62
theorem Th63: :: YELLOW_4:63
theorem :: YELLOW_4:64