Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-lcv Unicode version

Definition df-lcv 28477
 Description: Define the covering relation for subspaces of a left vector space. Similar to Definition 3.2.18 of [PtakPulmannova] p. 68. Ptak/Pulmannova's notation L is read " covers " or " is covered by " , and it means that is larger than and there is nothing in between. See lcvbr 28479 for binary relation. (df-cv 22852 analog.) (Contributed by NM, 7-Jan-2015.)
Assertion
Ref Expression
df-lcv L
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-lcv
StepHypRef Expression
1 clcv 28476 . 2 L
2 vw . . 3
3 cvv 2790 . . 3
4 vt . . . . . . . 8
54cv 1623 . . . . . . 7
62cv 1623 . . . . . . . 8
7 clss 15684 . . . . . . . 8
86, 7cfv 5222 . . . . . . 7
95, 8wcel 1685 . . . . . 6
10 vu . . . . . . . 8
1110cv 1623 . . . . . . 7
1211, 8wcel 1685 . . . . . 6
139, 12wa 360 . . . . 5
145, 11wpss 3155 . . . . . 6
15 vs . . . . . . . . . . 11
1615cv 1623 . . . . . . . . . 10
175, 16wpss 3155 . . . . . . . . 9
1816, 11wpss 3155 . . . . . . . . 9
1917, 18wa 360 . . . . . . . 8
2019, 15, 8wrex 2546 . . . . . . 7
2120wn 5 . . . . . 6
2214, 21wa 360 . . . . 5
2313, 22wa 360 . . . 4
2423, 4, 10copab 4078 . . 3
252, 3, 24cmpt 4079 . 2
261, 25wceq 1624 1 L
 Colors of variables: wff set class This definition is referenced by:  lcvfbr  28478
 Copyright terms: Public domain W3C validator