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

Definition df-ol 28535
Description: Define the class of ortholattices. Definition from [Kalmbach] p. 16. (Contributed by NM, 18-Sep-2011.)
Assertion
Ref Expression
df-ol  |-  OL  =  ( Lat  i^i  OP )

Detailed syntax breakdown of Definition df-ol
StepHypRef Expression
1 col 28531 . 2  class  OL
2 clat 14113 . . 3  class  Lat
3 cops 28529 . . 3  class  OP
42, 3cin 3126 . 2  class  ( Lat 
i^i  OP )
51, 4wceq 1619 1  wff  OL  =  ( Lat  i^i  OP )
Colors of variables: wff set class
This definition is referenced by:  isolat  28569
  Copyright terms: Public domain W3C validator