edges_transfer — Mathlib

English

The set of edges of a transferred walk is a subset of the original edge set mapped by f.

Русский

Множество ребер перенесённого обхода является образом подмножества исходного множества ребер через отображение f.

LaTeX

$$(p.transfer H hp).edgeSet = p.edgeSet$$

Lean4

@[simp]
theorem edges_transfer (hp) : (p.transfer H hp).edges = p.edges := by induction p <;> simp [*]

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