Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-lb Structured version   Visualization version   Unicode version

Definition df-lb 30691
Description: Define the lower bound relationship functor. See brlb 30770 for value. (Contributed by Scott Fenton, 3-May-2018.)
Assertion
Ref Expression
df-lb  |- LB R  = UB `' R

Detailed syntax breakdown of Definition df-lb
StepHypRef Expression
1 cR . . 3  class  R
21clb 30667 . 2  class LB R
31ccnv 4851 . . 3  class  `' R
43cub 30666 . 2  class UB `' R
52, 4wceq 1454 1  wff LB R  = UB `' R
Colors of variables: wff setvar class
This definition is referenced by:  brlb  30770
  Copyright terms: Public domain W3C validator