α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
h : Reflexive r
a b : α
hab : r a b
⊢ DirectedOn r {a, b}
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
h : Reflexive r
a b : α
hab : r a b
⊢ DirectedOn r {b, a}
rw [Set.pair_comm]
no goals
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
h : Reflexive r
a b : α
hab : r a b
⊢ DirectedOn r {a, b}
apply directedOn_pair h hab