of_apply_eq_base

Mathlib.GroupTheory.PushoutI

URI: https://scilib.ai/kg/mathlib#Monoid.PushoutI.of_apply_eq_base

English

Applying the i-th injection to φ_i x equals base φ x for any x in H.

Русский

Применение вводящего отображения i к элементу φ_i(x) равно базовому отображению φ x.

LaTeX

$$$of_i(\varphi_i(x)) = base(\varphi)(x)$ for all x ∈ H$$

Lean4

theorem of_apply_eq_base (i : ι) (x : H) : of i (φ i x) = base φ x := by rw [← MonoidHom.comp_apply, of_comp_eq_base]

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

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

Разделы

Аффилиация

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