Binary Relations

• Reflexive: ∀x:x~x
• Irreflexive: ∀x:x≁x
• Symmetric: ∀xy:xy→yx
• Antisymmetric: ∀xy:(x≠y∧xy)→yx
• Asymmetric: ∀xy:x~y→y≁x
• Transitive: ∀xyz:(x≁y∧y≁z)→x~z
• Total: ∀xy:xy∨yx
• Well-founded: ∀S≠∅ ∃m∈S ∀x∈S: s≁m, where S is a nonempty subset
• Has joins: ∀xy∃s: sx ∧ sy ∧ [∀w:(sx∧sy)→w~s]
• Has meets: ∀xy∃s: xs ∧ ys ∧ [∀w:(xs∧ys)→s~w]

	Reflexive	Irreflexive	Symmetric	Antisymmetric	Asymmetric	Transitive	Total	Well-founded	Has joins	Has meets