Description: Properties of greatest lower bound of a complete lattice. (Contributed by NM, 5-Dec-2011)
Ref | Expression | ||
---|---|---|---|
Hypotheses | clatglb.b | |
|
clatglb.l | |
||
clatglb.g | |
||
Assertion | clatglb | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | clatglb.b | |
|
2 | clatglb.l | |
|
3 | clatglb.g | |
|
4 | simpl | |
|
5 | 1 3 | clatglbcl2 | |
6 | 1 2 3 4 5 | glbprop | |