map_mem_edgeSet_iff — Mathlib

English

Let G and G' be simple graphs on vertex sets V and W, and f an embedding from G to G'. Then for every edge e in Sym^2 V, e.map f ∈ G'.edgeSet if and only if e ∈ G.edgeSet.

Русский

Пусть G и G' — простые графы на множествах вершин V и W, и f — вложение графов G в G'. Тогда для каждого ребра e ∈ Sym^2 V верно: e.map f ∈ edgeSet(G') тогда и только тогда e ∈ edgeSet(G).

LaTeX

$$$\forall e \in \mathrm{Sym}^2 V,\ e.map f \in G'.edgeSet \iff e \in G.edgeSet$$$

Lean4

theorem map_mem_edgeSet_iff {e : Sym2 V} : e.map f ∈ G'.edgeSet ↔ e ∈ G.edgeSet :=
  Sym2.ind (fun _ _ => f.map_adj_iff) e

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