Description: A Hilbert lattice satisfies the covering property of Definition 7.4 of MaedaMaeda p. 31 and its converse. ( cvp analog.) (Contributed by NM, 18-Nov-2011)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cvrp.b | |
|
cvrp.j | |
||
cvrp.m | |
||
cvrp.z | |
||
cvrp.c | |
||
cvrp.a | |
||
Assertion | cvrp | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cvrp.b | |
|
2 | cvrp.j | |
|
3 | cvrp.m | |
|
4 | cvrp.z | |
|
5 | cvrp.c | |
|
6 | cvrp.a | |
|
7 | hlomcmcv | |
|
8 | 1 2 3 4 5 6 | cvlcvrp | |
9 | 7 8 | syl3an1 | |