equalizer_le

Mathlib.CategoryTheory.Subpresheaf.Equalizer

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Subpresheaf.equalizer_le

English

The equalizer of f and g is a subpresheaf contained in A: equalizer f g ≤ A.

Русский

Равниитель f и g является подпрешафом, вложенным в A: равниитель f g ≤ A.

LaTeX

$$$\\text{equalizer}(f,g) \\le A$$$

Lean4

theorem equalizer_le : Subpresheaf.equalizer f g ≤ A := fun _ _ h ↦ h.1

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

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

Разделы

Аффилиация

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