Zulip Chat Archive

Stream: Is there code for X?

Topic: symmetric.iff

view this post on Zulip Jalex Stark (Jul 18 2020 at 22:55):

what should I use when I want to rw the symmetry of a symmetric relation?

lemma symmetric.iff {α : Type*} {r : α  α  Prop}
(h : symmetric r) (a b : α) : r a b  r b a :=
by split; apply h

view this post on Zulip Johan Commelin (Jul 19 2020 at 05:04):

I would guess there is a lemma close to the definition of symmetric.

view this post on Zulip Bryan Gin-ge Chen (Jul 19 2020 at 05:07):

symmetric is defined in core: docs#symmetric and there don't seem to be any lemmas about it there (nor in logic.basic or logic.relation).

Last updated: May 17 2021 at 16:26 UTC