adj_of_mem_incidenceSet — Mathlib

English

If a ≠ b and an edge e belongs to incidenceSet(a) and incidenceSet(b), then a and b are adjacent.

Русский

Если a ≠ b и ребро e принадлежит инцидентному множеству a и инцидентному множеству b, то a и b соседствуют.

LaTeX

$$$a \\neq b \\wedge e \\in G.incidenceSet(a) \\wedge e \\in G.incidenceSet(b) \\Rightarrow G.Adj(a,b)$$$

Lean4

theorem adj_of_mem_incidenceSet (h : a ≠ b) (ha : e ∈ G.incidenceSet a) (hb : e ∈ G.incidenceSet b) : G.Adj a b := by
  rwa [← mk'_mem_incidenceSet_left_iff, ←
    Set.mem_singleton_iff.1 <| G.incidenceSet_inter_incidenceSet_subset h ⟨ha, hb⟩]

Похожие утверждения