Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  df-cv Structured version   Visualization version   Unicode version

Definition df-cv 27932
 Description: Define the covers relation (on the Hilbert lattice). Definition 3.2.18 of [PtakPulmannova] p. 68, whose notation we use. Ptak/Pulmannova's notation is read " covers " or " is covered by " , and it means that is larger than and there is nothing in between. See cvbr 27935 and cvbr2 27936 for membership relations. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.)
Assertion
Ref Expression
df-cv
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-cv
StepHypRef Expression
1 ccv 26617 . 2
2 vx . . . . . . 7
32cv 1443 . . . . . 6
4 cch 26582 . . . . . 6
53, 4wcel 1887 . . . . 5
6 vy . . . . . . 7
76cv 1443 . . . . . 6
87, 4wcel 1887 . . . . 5
95, 8wa 371 . . . 4
103, 7wpss 3405 . . . . 5
11 vz . . . . . . . . . 10
1211cv 1443 . . . . . . . . 9
133, 12wpss 3405 . . . . . . . 8
1412, 7wpss 3405 . . . . . . . 8
1513, 14wa 371 . . . . . . 7
1615, 11, 4wrex 2738 . . . . . 6
1716wn 3 . . . . 5
1810, 17wa 371 . . . 4
199, 18wa 371 . . 3
2019, 2, 6copab 4460 . 2
211, 20wceq 1444 1
 Colors of variables: wff setvar class This definition is referenced by:  cvbr  27935
 Copyright terms: Public domain W3C validator