vertex in edge if edge in incidence set

Stream: Is there code for X?

[Christoph Spiegel]

Does anything like this exist for SimpleGraph?

@[simp] lemma mem_incidenceSet_iff_mem_edge (v : α) {e : Sym2 α} (he : e ∈ E) :
    v ∈ e ↔ e ∈ G.incidenceSet v := by
  simp [SimpleGraph.incidenceSet]
  exact λ _ ↦ SimpleGraph.mem_edgeFinset.mp he

@[simp] lemma mem_incidenceFinset_iff_mem_edge (v : α) {e : Sym2 α} (he : e ∈ E) :
    v ∈ e ↔ e ∈ G.incidenceFinset v := by
  simp [SimpleGraph.incidenceFinset, SimpleGraph.incidenceSet]
  exact λ _ ↦ SimpleGraph.mem_edgeFinset.mp he

[Yakov Pechersky]

I would expect such lemmas to have the iff direction reversed, this having the simpler expression on the RHS. Looking at the definitions, I would hope simp [incidenceSet, he] would suffice

[Christoph Spiegel]

The set version can be closed with just simp, I was just incorrectly using edgeFinset instead of edgeSet. The finset version seems to require exact. Minimum working code:

import Mathlib.Combinatorics.SimpleGraph.Finite

variable {α : Type*}
variable {G : SimpleGraph α}

lemma mem_edge_iff_mem_incidenceSet (v : α) {e : Sym2 α} (he : e ∈ G.edgeSet) :
    e ∈ G.incidenceSet v ↔ v ∈ e := by
  simp [SimpleGraph.incidenceSet, he]

variable [Fintype α] [DecidableEq α] [DecidableRel G.Adj]

lemma mem_edgeFinset_iff_mem_incidenceFinset (v : α) {e : Sym2 α} (he : e ∈  G.edgeFinset) :
    e ∈ G.incidenceFinset v ↔ v ∈ e := by
  simp [SimpleGraph.incidenceFinset, SimpleGraph.incidenceSet]
  exact λ _ ↦ SimpleGraph.mem_edgeFinset.mp he

[Yakov Pechersky]

Use mem_edgeFinset to rewrite your he hypothesis, then you can use it with your lemma above and the unfolding of the incidenceFinset definition.

[Yakov Pechersky]

In fact, the whole proof for the second lemma might be a term mode usage of the first lemma

[Christoph Spiegel]

Alright, so this works:

import Mathlib.Combinatorics.SimpleGraph.Finite

variable {α : Type*}
variable {G : SimpleGraph α}

lemma mem_edge_iff_mem_incidenceSet (v : α) {e : Sym2 α} (he : e ∈ G.edgeSet) :
    e ∈ G.incidenceSet v ↔ v ∈ e := by
  simp [SimpleGraph.incidenceSet, he]

variable [Fintype α] [DecidableEq α] [DecidableRel G.Adj]

lemma mem_edgeFinset_iff_mem_incidenceFinset (v : α) {e : Sym2 α} (he : e ∈  G.edgeFinset) :
    e ∈ G.incidenceFinset v ↔ v ∈ e := by
  rw [SimpleGraph.mem_edgeFinset] at he
  simp [mem_edge_iff_mem_incidenceSet, he]

[Christoph Spiegel]

Does it make sense to PR it?

[Yaël Dillies]

Can you not strengthen the first one to e ∈ G.incidenceSet v ↔ v ∈ e ∧ e ∈ G.edgeSet?

[Yakov Pechersky]

I think that is Iff.rfl

[Yakov Pechersky]

Btw, Christoph, you should be able to have v as an implicit argument in your statements -- that's the usual style for iffs, since it appears in the statement (especially on both sides)