condition

Mathlib.Logic.Function.Coequalizer

URI: https://scilib.ai/kg/mathlib#Function.Coequalizer.condition

← MathLib Explorer

English

For any f,g : α → β, mk f g (f x) = mk f g (g x) for all x.

Русский

Для любых f,g : α → β верно mk f g (f x) = mk f g (g x) для всех x.

LaTeX

$$$ \forall {\alpha} {\beta} (f g : \alpha \to \beta) (x : \alpha),\; \operatorname{Function.Coequalizer}.mk f g (f x) = \operatorname{Function.Coequalizer}.mk f g (g x)$$$

Lean4

theorem condition (x : α) : mk f g (f x) = mk f g (g x) :=
  Quot.sound (.intro x)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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