df-klojere - brismu bridi

	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-klojere	⊢ go 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)

W3C validator