def Rel.union {α : Type u_1} {β : Type u_2} (r s : Rel α β) : Rel α β

Union of two relations.

Equations

• r.union s x y = (r x y ∨ s x y)

def Rel.upTo {α : Type u_1} (r s : Rel α α) : Rel α α

The relation r 'up to' the relation s.

Equations

• r.upTo s = s.comp (r.comp s)

inductive Rel.Id {α : Type u_1} : Rel α α

The identity relation.

• id {α : Type u_1} {x : α} : Id x x