# Zulip Chat Archive

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

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

#### 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 : α)
def link.rev (x : link α β) : link α β := ⟨x.dest, x.via, x.src⟩
```

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.

Thanks for the advice everyone.

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

Yeah, just use what you wrote. It's fine.

Last updated: May 19 2021 at 02:10 UTC