## Stream: Is there code for X?

### Topic: symmetric.iff

#### 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


#### Johan Commelin (Jul 19 2020 at 05:04):

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

#### 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