# Zulip Chat Archive

## Stream: new members

### Topic: edge_set for Digraphs

#### Christopher Schmidt (Jan 08 2023 at 15:00):

Hello everyone, I am working on directed Graphs and I am trying to analogously (to simple_graph) introduce a bunch of stuff.

Right now I am trying to get and analogue to :

```
def edge_set : simple_graph V ↪o set (sym2 V) :=
order_embedding.of_map_le_iff (λ G, sym2.from_rel G.symm) $
λ G G', ⟨λ h a b, @h ⟦(a, b)⟧, λ h e, sym2.ind @h e⟩
```

Here an mwe :

```
universe u
@[ext]
structure directed_simple_graph (V : Type u) := (adj : V → V → Prop)
namespace directed_simple_graph
variables {V : Type u}
variables (G : directed_simple_graph V)
def edge_set : directed_simple_graph V ↪ set (V × V) := \lambda G, sorry
```

I am a little lost on how to implement the idea that set(V \times V) is supposed to include all v1 v2 : V that fulfill G.adj

Any help is appreciated.

#### Kyle Miller (Jan 09 2023 at 10:30):

@Christopher Schmidt Here's an order embedding:

```
universe u
@[ext]
structure directed_simple_graph (V : Type u) := (adj : V → V → Prop)
namespace directed_simple_graph
variables {V : Type u}
variables (G : directed_simple_graph V)
-- Give `directed_simple_graph V` the induced partial order from the one already
-- defined on `V → V → Prop`
instance : partial_order (directed_simple_graph V) := partial_order.lift adj ext
def edge_set : directed_simple_graph V ↪o set (V × V) :=
order_embedding.of_map_le_iff (λ (G : directed_simple_graph V), {p : V × V | G.adj p.1 p.2}) $
begin
intros G G',
rw [le_eq_subset, set_of_subset_set_of, prod.forall],
refl,
end
end directed_simple_graph
```

#### Kyle Miller (Jan 09 2023 at 10:35):

Here's just an embedding:

```
def edge_set : directed_simple_graph V ↪ set (V × V) :=
{ to_fun := λ G, {p : V × V | G.adj p.1 p.2},
inj' := begin
intros G G' h,
simp only [set.ext_iff] at h,
ext u v,
specialize h (u, v),
exact h,
end }
```

It takes a different proof since `order_embedding.of_map_le_iff`

is able to prove the injectivity condition using a order-based principle.

#### Kyle Miller (Jan 09 2023 at 10:37):

Here's a plain function:

```
def edge_set : directed_simple_graph V → set (V × V) :=
λ G, {p : V × V | G.adj p.1 p.2}
```

Not too long ago docs#simple_graph.edge_set used to be a plain function

#### Christopher Schmidt (Jan 09 2023 at 21:28):

Thank you so much @Kyle Miller .

However, I have got a question. What is the difference between the embedding and the plain function when it comes to the use of G.edge_set ? Don't both just provide the same result ?

#### Kyle Miller (Jan 09 2023 at 22:35):

They all give the same functions, but the embeddings "bundle" additional proofs with the functions, which can make general lemmas about them become more easily available.

Otherwise, you can give extra lemmas about edge sets yourself. (The "unbundled" approach.)

I'm not sure exactly if there are applications of bundled edge sets in mathlib yet.

#### Christopher Schmidt (Jan 10 2023 at 09:13):

Ah I see. Thank you.

Last updated: Dec 20 2023 at 11:08 UTC