transfer_eq_map_ofLE — Mathlib

English

Same as transfer toLE, with a different naming convention; the transferred walk equals the mapped walk using LE inclusions.

Русский

То же, что и перенос через LE, но с другой нотацией; перенесённый обход равен отображённому обходу через включения LE.

LaTeX

$$p.transfer H hp = p.map (SimpleGraph.Hom.ofLE GH)$$

Lean4

theorem transfer_eq_map_ofLE (hp) (GH : G ≤ H) : p.transfer H hp = p.map (.ofLE GH) := by induction p <;> simp [*]

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