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

Definition df-lb 30642
Description: Define the lower bound relationship functor. See brlb 30721 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 30618 . 2  class LB R
31ccnv 4850 . . 3  class  `' R
43cub 30617 . 2  class UB `' R
52, 4wceq 1438 1  wff LB R  = UB `' R
Colors of variables: wff setvar class
This definition is referenced by:  brlb  30721
  Copyright terms: Public domain W3C validator