df-klojere - brismu bridi

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

Definition df-klojere 509

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 1 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 1 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