mem_equalizer_iff

Mathlib.CategoryTheory.Subpresheaf.Equalizer

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

English

A point x at i belongs to the equalizer iff f.app i x = g.app i x.

Русский

Точка x при i принадлежит равнителю тогда и только тогда, когда f.app i x = g.app i x.

LaTeX

$$$x.1 \\in (\\text{Subpresheaf.equalizer } f g).obj i \\iff f.app i x = g.app i x$$$

Lean4

theorem mem_equalizer_iff {i : Cᵒᵖ} (x : A.toPresheaf.obj i) :
    x.1 ∈ (Subpresheaf.equalizer f g).obj i ↔ f.app i x = g.app i x := by simp

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

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

Разделы

Аффилиация

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