# Zulip Chat Archive

## Stream: graph theory

### Topic: Creating an edge from vertices

#### Gabriel Moise (Apr 02 2021 at 08:52):

Hello!

I was trying some proofs and lemmas about the incidence matrix of a graph, and I would find it useful if I could have a definition of an edge from the 2 given vertices, knowing the fact that they are adjacent in the graph. I tried something like this

```
import linear_algebra.matrix
import combinatorics.simple_graph.basic
open_locale big_operators matrix
open finset matrix simple_graph
universes u v
variables {V : Type u} [fintype V]
namespace simple_graph
variables (G : simple_graph V) [decidable_rel G.adj] [decidable_eq V]
def edge_from_vertices (i j : V) (H_adj : G.adj i j) : G.edge_set := ⟦(i,j)⟧
end simple_graph
```

However, there is a problem because Lean can't coerce the ⟦(i,j)⟧ into a member of the G.edge_set. Has anyone encountered this and has a solution? I would like to have something like, the edge_from_vertices i j H_adj would be

e such that e.val = ⟦(i,j)⟧, but I don't know how to define that.

#### Eric Rodriguez (Apr 02 2021 at 09:44):

I'm confused what you mean; isn't `G.adj i j`

evidence that `i j`

is an edge? Can you post a #mwe explaining what you need it for?

#### Alena Gusakov (Apr 02 2021 at 09:57):

I'm pretty sure there's a lemma stating that there exists an edge iff adjacent, you might be able to use that?

#### Gabriel Moise (Apr 02 2021 at 09:57):

I wasn't talking about the evidence that (i,j) represents an edge, I was talking about having the edge as an object and using it for calculations, for instance:

```
lemma filter_edge_card_one {i j : V} (H_adj : G.adj i j) :
filter (λ (x : (G.edge_set)), ↑x = ⟦(i, j)⟧) univ = {G.edge_from_vertices i j H_adj} :=
begin
sorry
end
```

#### Alena Gusakov (Apr 02 2021 at 10:00):

I think you can use the existence lemma to create the edge but I'm not currently able to test it (it's like 6 am where I am sorry lol)

#### Alena Gusakov (Apr 02 2021 at 10:02):

I think I get what you're saying though - G.edge_set isn't a type, so you can't say def etc : G.edge_set := ...

#### Eric Wieser (Apr 02 2021 at 10:02):

Sure you can, because docs#set.has_coe_to_sort exists? (although you probably shouldn't!)

#### Alena Gusakov (Apr 02 2021 at 10:02):

You can do def etc : sym2 V := ... because that's the type of edges

#### Eric Wieser (Apr 02 2021 at 10:03):

`filter (λ (x : (G.edge_set)), ↑x = ⟦(i, j)⟧) univ`

should be the same as `filter (λ (x : sym2 V), x = ⟦(i, j)⟧) G.edge_set`

, and the latter will be easier to work with

#### Gabriel Moise (Apr 02 2021 at 10:04):

Well, I am sure that there is a possibility, but I am not very accustomed to working with coercions, although I stumble upon them a lot, so I wanted to see an example so that I can understand more.

#### Eric Wieser (Apr 02 2021 at 10:05):

At a guess you're looking for

```
def edge_from_vertices (i j : V) (H_adj : G.adj i j) : G.edge_set := ⟨⟦(i,j)⟧, H_adj⟩
```

#### Eric Wieser (Apr 02 2021 at 10:08):

Or another way to write it, without exploiting that docs#sym2.from_rel_prop is true by `rfl`

:

```
def edge_from_vertices (i j : V) (H_adj : G.adj i j) : G.edge_set :=
⟨_, sym2.from_rel_prop.mpr H_adj⟩
```

#### Gabriel Moise (Apr 02 2021 at 10:09):

Can you explain a little how does the construction work (⟨⟦(i,j)⟧, H_adj⟩) ?

#### Eric Wieser (Apr 02 2021 at 10:10):

`↥G.edge_set`

is short for `{x // x ∈ G.edge_set}`

aka `subtype (∈ G.edge_set)`

. `subtype x`

is just a pair of `x`

and `p x`

(docs#subtype)

#### Eric Wieser (Apr 02 2021 at 10:11):

Conveniently, it turns out the statements `⟦(i,j)⟧ ∈ G.edge_set`

and `G.adj i j`

are defeq, so as long as lean already knows what type it's looking for, you can supply a proof of the latter (`H_adj`

) where the former is expected.

#### Gabriel Moise (Apr 02 2021 at 10:13):

Oh, I think I see what you mean. Thank you very much! I am currently working on proving more lemmas and I might have more questions, I will use this topic for that, if that's ok :smile:

Last updated: Dec 20 2023 at 11:08 UTC