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

Definition df-cv 23782
 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 23785 and cvbr2 23786 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 22467 . 2
2 vx . . . . . . 7
32cv 1651 . . . . . 6
4 cch 22432 . . . . . 6
53, 4wcel 1725 . . . . 5
6 vy . . . . . . 7
76cv 1651 . . . . . 6
87, 4wcel 1725 . . . . 5
95, 8wa 359 . . . 4
103, 7wpss 3321 . . . . 5
11 vz . . . . . . . . . 10
1211cv 1651 . . . . . . . . 9
133, 12wpss 3321 . . . . . . . 8
1412, 7wpss 3321 . . . . . . . 8
1513, 14wa 359 . . . . . . 7
1615, 11, 4wrex 2706 . . . . . 6
1716wn 3 . . . . 5
1810, 17wa 359 . . . 4
199, 18wa 359 . . 3
2019, 2, 6copab 4265 . 2
211, 20wceq 1652 1
 Colors of variables: wff set class This definition is referenced by:  cvbr  23785
 Copyright terms: Public domain W3C validator