## Stream: Is there code for X?

### Topic: Injective on a set up to a relation

#### Kyle Miller (Jun 25 2020 at 18:38):

I couldn't find a definition like the following in mathlib:

universes u v
variables {α : Type u} {β : Type v}

@[reducible] def inj_on_by (f : α → β) (s : set α) (r : α → α → Prop) : Prop :=
∀⦃x₁ x₂ : α⦄, x₁ ∈ s → x₂ ∈ s → f x₁ = f x₂ → r x₁ x₂


(this is a variation on set.inj_on in data/set/function.lean). For the particular use I have in mind, α has a setoid instance, in case that matters.

So, (1) is there some other definition I should be using? or, barring that, (2) would this function be welcome in data/set/function.lean or elsewhere?

#### Patrick Massot (Jun 25 2020 at 18:40):

This looks very specialized.

#### Reid Barton (Jun 25 2020 at 18:41):

inj_on is already pretty obscure, I would say

#### Johan Commelin (Jun 25 2020 at 18:43):

@Kyle Miller I guess you want to use this in your graph theory stuff, right? Could you explain a bit more how/why?

#xy

#### Kyle Miller (Jun 25 2020 at 19:07):

@Johan Commelin One of the axioms for undirected graphs in the Chou formalization is exactly inj_on_by link.via links (≈), where links is a set of link elements, defined by

structure link (α : Type u) (β : Type v) :=
(src : α) (via : β) (dest : α)



with an equivalence relation given by

def same_edge : link α β → link α β → Prop := λ x y, x = y ∨ x = y.rev


That is, if two links carry the same edge (have the same via), then they are equal up to orientation reversal.

It's not essential that this definition actually exists, and I'm fine with writing out the full definition of the axiom in the structure. This would be the only one of the three axioms involving any quantifiers.

In the context of all the axioms, we want link.via on the links set to have link.rev acting on its fibers.

Another way of thinking about this particular axiom is that link.via descends to a map on the quotient of link α β by same_edge, and we wish for this map to be injective. It seems like it would be more trouble than it's worth to use quotient types to specify this axiom.

#### Johan Commelin (Jun 25 2020 at 19:15):

I think it's easiest to just write it out

#### Johan Commelin (Jun 25 2020 at 19:16):

\forall x y, x.via = y.via → same_edge x y
is that what you want, or am I missing something?

#### Kyle Miller (Jun 25 2020 at 19:43):

Since there's a set of links, it would be

∀ {x y}, x ∈ links → y ∈ links → x.via = y.via → same_edge x y


but yeah, that's pretty much it.

I just thought I'd ask in case this was somehow less specialized than I imagined it to be, or if there was some convenient setoid thing I didn't know about.