equalizer_self

Mathlib.CategoryTheory.Subpresheaf.Equalizer

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

English

The equalizer of f with itself is exactly the subpresheaf A: equalizer f f = A.

Русский

Равнитель f и f равен подпрешафу A: equalizer f f = A.

LaTeX

$$$\\text{equalizer}(f,f) = A$$$

Lean4

@[simp]
theorem equalizer_self : Subpresheaf.equalizer f f = A := by aesop

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

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

Разделы

Аффилиация

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