QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  df-le Unicode version
Definition df-le 129
Description: Define 'less than or equal to' analogue.
Assertion
Ref Expression
df-le (a =<2 b) = ((a v b) == b)
Detailed syntax breakdown of Definition df-le
StepHypRef Expression
1 wva . . 3 term a
2 wvb . . 3 term b
31, 2wle2 10 . 2 term (a =<2 b)
41, 2wo 6 . . 3 term (a v b)
54, 2tb 5 . 2 term ((a v b) == b)
63, 5wb 1 1 wff (a =<2 b) = ((a v b) == b)
Colors of variables: term
This definition is referenced by:  lei2  346  wdf-le1  378  wdf-le2  379  wle0  390  wler  391
  Copyright terms: Public domain W3C validator