edgeSet_coe — Mathlib

English

The edge set of the coe-subgraph is the preimage of the subgraph's edge set under the map that takes a pair to its underlying pair of vertices.

Русский

Множество ребер подграфа, полученное через вложение, является предварительным образом множества ребер подграфа, когда применяется отображение на исходные вершины.

LaTeX

$$$G'.coe.edgeSet = \\mathrm{Sym2.map}(\\mathrm{Subtype.val})^{-1}(G'.edgeSet)$$$

Lean4

@[simp]
theorem edgeSet_coe {G' : G.Subgraph} : G'.coe.edgeSet = Sym2.map (↑) ⁻¹' G'.edgeSet := by ext e;
  induction e using Sym2.ind; simp

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