symmetric.on

Stream: Is there code for X?

[Yakov Pechersky]

Do we have something that gives that when r is a symmetric relation, so is r on f? Here's a mwe for why I need it:

import data.multiset.basic
import order.bounded

variables {α β : Type*} [semilattice_inf α] [order_bot α] (x y : α) (f : β → α) (n m : β)

example : disjoint x y → disjoint y x := λ h, symmetric_disjoint h

example : disjoint x y → disjoint y x := by apply symmetric_disjoint

-- This works
example : (disjoint on f) n m → (disjoint on f) m n := λ h, symmetric_disjoint h

-- So does this
example : (disjoint on f) n m → (disjoint on f) m n := by apply symmetric_disjoint

example (l : list β) : multiset.pairwise (disjoint on f) ↑l :=
begin
  rw multiset.pairwise_coe_iff_pairwise,
  sorry,
  exact symmetric_disjoint -- doesn't work here
end

-- but it could if we had:
def symmetric.on {r : α → α → Prop} (h : symmetric r) : symmetric (r on f) :=
λ x y hxy, h hxy

example (l : list β) : multiset.pairwise (disjoint on f) ↑l :=
begin
  rw multiset.pairwise_coe_iff_pairwise (symmetric_disjoint.on f), -- now it works
  sorry,
end

[Yakov Pechersky]

And if I add this, where do I put it? Both docs#function.on_fun and docs#symmetric are in core.

[Yakov Pechersky]

It's docs#symmetric.comap. I was already using it in another lemma! Whoops.

[Yury G. Kudryashov]

You can add an alias symmetric.on_fun if you want.