coe_induceHom

Mathlib.Combinatorics.SimpleGraph.Maps

URI: https://scilib.ai/kg/mathlib#SimpleGraph.coe_induceHom

English

The underlying function of induceHom φ φst equals the restriction Set.MapsTo.restrict φ s t φst.

Русский

Базовая функция induceHom φ φst равна ограничению Set.MapsTo.restrict φ s t φst.

LaTeX

$$$ \operatorname{coe}(\mathrm{induceHom}(\phi,\phi_{st})) = \mathrm{Set.MapsTo.restrict}(\phi,s,t,\phi_{st}) $$$

Lean4

@[simp, norm_cast]
theorem coe_induceHom : ⇑(induceHom φ φst) = Set.MapsTo.restrict φ s t φst :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru