Home brismu bridi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >   Home  >  Th. List  >  df-klojere

Definition df-klojere 564
Description: Definition of {klojere}. This is our most foundational definition for binary operators for now: a binary operator is a ternary relation closed over a set such that, for every ordered pair of elements in the closure, there is a unique related element. In terms of abstract algebra, our binary operators are magmas.
Assertion
Ref Expression
df-klojerego pa ka ce'u bu'a ce'u ce'u kei klojere ko'a gi ro da poi ke'a cmima ko'a ku'o zo'u ro de poi ke'a cmima ko'a ku'o zo'u pa di poi ke'a cmima ko'a ku'o zo'u da bu'a de di
Distinct variable group:   da , de , di

This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator