The asymmetric part of a relation [UPSTREAM]

The asymmetric part of a relation r holds of a and b when r a b holds and r b a does not. It is the strict counterpart of mathlib's AntisymmRel, the symmetric part, and on a preorder it is <. Social choice reads it as strict preference when r is weak preference.

Upstream home: Mathlib/Order/Antisymmetrization.lean, beside AntisymmRel.

Main definitions

• AsymmRel: the asymmetric part of a relation.

def AsymmRel {α : Type u_1} (r : α → α → Prop) (a b : α) : Prop

The asymmetric part of a relation holds of a and b when r a b and not r b a. Mathlib's AntisymmRel r is the symmetric part.

Equations

• AsymmRel r a b = (r a b ∧ ¬r b a)

@[instance_reducible]

instance instDecidableAsymmRelOfDecidableRel {α : Type u_1} (r : α → α → Prop) [DecidableRel r] (a b : α) : Decidable (AsymmRel r a b)

Equations

• instDecidableAsymmRelOfDecidableRel r a b = { decide := decide (r a b) && decide ¬r b a, reflects_decide := ⋯ }

theorem AsymmRel.trans_le {α : Type u_1} {r : α → α → Prop} [IsTrans α r] {a b c : α} (h : AsymmRel r a b) (h' : r b c) : AsymmRel r a c