:: Bounds in Posets and Relational Substructures
:: by Grzegorz Bancerek
::
:: Received September 10, 1996
:: Copyright (c) 1996 Association of Mizar Users
:: deftheorem defines reflexive YELLOW_0:def 1 :
:: deftheorem defines transitive YELLOW_0:def 2 :
:: deftheorem defines antisymmetric YELLOW_0:def 3 :
theorem Th1: :: YELLOW_0:1
theorem Th2: :: YELLOW_0:2
theorem :: YELLOW_0:3
theorem Th4: :: YELLOW_0:4
theorem Th5: :: YELLOW_0:5
theorem Th6: :: YELLOW_0:6
theorem Th7: :: YELLOW_0:7
theorem Th8: :: YELLOW_0:8
theorem Th9: :: YELLOW_0:9
theorem Th10: :: YELLOW_0:10
theorem Th11: :: YELLOW_0:11
theorem Th12: :: YELLOW_0:12
:: deftheorem Def4 defines lower-bounded YELLOW_0:def 4 :
:: deftheorem Def5 defines upper-bounded YELLOW_0:def 5 :
:: deftheorem defines bounded YELLOW_0:def 6 :
theorem :: YELLOW_0:13
:: deftheorem Def7 defines ex_sup_of YELLOW_0:def 7 :
:: deftheorem Def8 defines ex_inf_of YELLOW_0:def 8 :
theorem Th14: :: YELLOW_0:14
theorem Th15: :: YELLOW_0:15
theorem Th16: :: YELLOW_0:16
theorem Th17: :: YELLOW_0:17
theorem Th18: :: YELLOW_0:18
theorem Th19: :: YELLOW_0:19
theorem Th20: :: YELLOW_0:20
theorem Th21: :: YELLOW_0:21
theorem Th22: :: YELLOW_0:22
theorem Th23: :: YELLOW_0:23
theorem :: YELLOW_0:24
theorem :: YELLOW_0:25
definition
let L be
RelStr ;
let X be
set ;
func "\/" X,
L -> Element of
L means :
Def9:
:: YELLOW_0:def 9
(
X is_<=_than it & ( for
a being
Element of
L st
X is_<=_than a holds
it <= a ) )
if ex_sup_of X,
L;
uniqueness
for b1, b2 being Element of L st ex_sup_of X,L & X is_<=_than b1 & ( for a being Element of L st X is_<=_than a holds
b1 <= a ) & X is_<=_than b2 & ( for a being Element of L st X is_<=_than a holds
b2 <= a ) holds
b1 = b2
existence
( ex_sup_of X,L implies ex b1 being Element of L st
( X is_<=_than b1 & ( for a being Element of L st X is_<=_than a holds
b1 <= a ) ) )
correctness
consistency
for b1 being Element of L holds verum;
;
func "/\" X,
L -> Element of
L means :
Def10:
:: YELLOW_0:def 10
(
X is_>=_than it & ( for
a being
Element of
L st
X is_>=_than a holds
a <= it ) )
if ex_inf_of X,
L;
uniqueness
for b1, b2 being Element of L st ex_inf_of X,L & X is_>=_than b1 & ( for a being Element of L st X is_>=_than a holds
a <= b1 ) & X is_>=_than b2 & ( for a being Element of L st X is_>=_than a holds
a <= b2 ) holds
b1 = b2
existence
( ex_inf_of X,L implies ex b1 being Element of L st
( X is_>=_than b1 & ( for a being Element of L st X is_>=_than a holds
a <= b1 ) ) )
correctness
consistency
for b1 being Element of L holds verum;
;
end;
:: deftheorem Def9 defines "\/" YELLOW_0:def 9 :
:: deftheorem Def10 defines "/\" YELLOW_0:def 10 :
theorem :: YELLOW_0:26
theorem :: YELLOW_0:27
theorem :: YELLOW_0:28
theorem :: YELLOW_0:29
theorem Th30: :: YELLOW_0:30
theorem Th31: :: YELLOW_0:31
theorem :: YELLOW_0:32
theorem :: YELLOW_0:33
theorem Th34: :: YELLOW_0:34
theorem Th35: :: YELLOW_0:35
theorem :: YELLOW_0:36
theorem :: YELLOW_0:37
theorem Th38: :: YELLOW_0:38
theorem :: YELLOW_0:39
theorem Th40: :: YELLOW_0:40
theorem Th41: :: YELLOW_0:41
theorem Th42: :: YELLOW_0:42
theorem Th43: :: YELLOW_0:43
:: deftheorem defines Bottom YELLOW_0:def 11 :
:: deftheorem defines Top YELLOW_0:def 12 :
theorem :: YELLOW_0:44
theorem :: YELLOW_0:45
theorem Th46: :: YELLOW_0:46
theorem Th47: :: YELLOW_0:47
theorem Th48: :: YELLOW_0:48
theorem Th49: :: YELLOW_0:49
theorem Th50: :: YELLOW_0:50
theorem :: YELLOW_0:51
theorem :: YELLOW_0:52
theorem :: YELLOW_0:53
theorem :: YELLOW_0:54
theorem :: YELLOW_0:55
:: deftheorem Def13 defines SubRelStr YELLOW_0:def 13 :
:: deftheorem Def14 defines full YELLOW_0:def 14 :
theorem :: YELLOW_0:56
canceled;
theorem Th57: :: YELLOW_0:57
theorem Th58: :: YELLOW_0:58
:: deftheorem defines subrelstr YELLOW_0:def 15 :
theorem Th59: :: YELLOW_0:59
theorem Th60: :: YELLOW_0:60
theorem Th61: :: YELLOW_0:61
theorem Th62: :: YELLOW_0:62
theorem Th63: :: YELLOW_0:63
:: deftheorem Def16 defines meet-inheriting YELLOW_0:def 16 :
:: deftheorem Def17 defines join-inheriting YELLOW_0:def 17 :
:: deftheorem defines infs-inheriting YELLOW_0:def 18 :
:: deftheorem defines sups-inheriting YELLOW_0:def 19 :
theorem Th64: :: YELLOW_0:64
theorem Th65: :: YELLOW_0:65
theorem :: YELLOW_0:66
for
L being non
empty transitive RelStr for
S being non
empty full SubRelStr of
L for
x,
y being
Element of
S st
ex_inf_of {x,y},
L &
"/\" {x,y},
L in the
carrier of
S holds
(
ex_inf_of {x,y},
S &
"/\" {x,y},
S = "/\" {x,y},
L )
by Th64;
theorem :: YELLOW_0:67
for
L being non
empty transitive RelStr for
S being non
empty full SubRelStr of
L for
x,
y being
Element of
S st
ex_sup_of {x,y},
L &
"\/" {x,y},
L in the
carrier of
S holds
(
ex_sup_of {x,y},
S &
"\/" {x,y},
S = "\/" {x,y},
L )
by Th65;
theorem :: YELLOW_0:68
theorem :: YELLOW_0:69
theorem :: YELLOW_0:70
theorem :: YELLOW_0:71