factorsThrough

Mathlib.Logic.Function.Basic

URI: https://scilib.ai/kg/mathlib#Function.Injective.factorsThrough

English

If g factors through f, then extend f g e' applied to any a equals g a when evaluated at f a.

Русский

Если g факторизуется через f, то extend f g e' на f a даёт g a.

LaTeX

$$$\text{If } g = h \circ f \text{ for some } h,\quad \operatorname{extend} f g e' (f a) = g a$$$

Lean4

theorem factorsThrough (hf : Injective f) (g : α → γ) : g.FactorsThrough f := fun _ _ h => congr_arg g (hf h)

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

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

Разделы

Аффилиация

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