:: The Properties of Product of Relational Structures
:: by Artur Korni{\l}owicz
::
:: Received March 27, 1998
:: Copyright (c) 1998 Association of Mizar Users
theorem :: YELLOW10:1
theorem :: YELLOW10:2
theorem Th3: :: YELLOW10:3
theorem Th4: :: YELLOW10:4
theorem Th5: :: YELLOW10:5
theorem :: YELLOW10:6
theorem :: YELLOW10:7
theorem :: YELLOW10:8
theorem :: YELLOW10:9
theorem :: YELLOW10:10
theorem :: YELLOW10:11
for
S,
T being non
empty antisymmetric RelStr for
x,
y being
Element of
[:S,T:] holds
(
ex_inf_of {x,y},
[:S,T:] iff (
ex_inf_of {(x `1 ),(y `1 )},
S &
ex_inf_of {(x `2 ),(y `2 )},
T ) )
theorem :: YELLOW10:12
for
S,
T being non
empty antisymmetric RelStr for
x,
y being
Element of
[:S,T:] holds
(
ex_sup_of {x,y},
[:S,T:] iff (
ex_sup_of {(x `1 ),(y `1 )},
S &
ex_sup_of {(x `2 ),(y `2 )},
T ) )
theorem Th13: :: YELLOW10:13
theorem Th14: :: YELLOW10:14
theorem Th15: :: YELLOW10:15
theorem Th16: :: YELLOW10:16
theorem Th17: :: YELLOW10:17
theorem Th18: :: YELLOW10:18
theorem Th19: :: YELLOW10:19
theorem Th20: :: YELLOW10:20
theorem Th21: :: YELLOW10:21
theorem Th22: :: YELLOW10:22
theorem Th23: :: YELLOW10:23
theorem Th24: :: YELLOW10:24
theorem :: YELLOW10:25
theorem :: YELLOW10:26
theorem :: YELLOW10:27
theorem Th28: :: YELLOW10:28
theorem :: YELLOW10:29
theorem :: YELLOW10:30
theorem :: YELLOW10:31
theorem :: YELLOW10:32
theorem Th33: :: YELLOW10:33
theorem :: YELLOW10:34
theorem :: YELLOW10:35
theorem :: YELLOW10:36
theorem Th37: :: YELLOW10:37
theorem :: YELLOW10:38
theorem :: YELLOW10:39
theorem :: YELLOW10:40
theorem Th41: :: YELLOW10:41
theorem :: YELLOW10:42
theorem :: YELLOW10:43
theorem Th44: :: YELLOW10:44
theorem Th45: :: YELLOW10:45
theorem Th46: :: YELLOW10:46
theorem Th47: :: YELLOW10:47
theorem :: YELLOW10:48
theorem :: YELLOW10:49
theorem Th50: :: YELLOW10:50
theorem Th51: :: YELLOW10:51
theorem Th52: :: YELLOW10:52
theorem Th53: :: YELLOW10:53
theorem :: YELLOW10:54
theorem :: YELLOW10:55
theorem :: YELLOW10:56
theorem :: YELLOW10:57
theorem :: YELLOW10:58
theorem :: YELLOW10:59
theorem :: YELLOW10:60
theorem :: YELLOW10:61
theorem Th62: :: YELLOW10:62
theorem :: YELLOW10:63
theorem :: YELLOW10:64
theorem :: YELLOW10:65
theorem :: YELLOW10:66
theorem :: YELLOW10:67
theorem :: YELLOW10:68
theorem Th69: :: YELLOW10:69
theorem :: YELLOW10:70