equalizerSieve_self_eq_top

Mathlib.CategoryTheory.Sites.LocallyInjective

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Presheaf.equalizerSieve_self_eq_top

English

For any presheaf F with suitable structure, the equalizer sieve of x against itself is the top sieve.

Русский

Для любой предрассевы F равное сито против самого себя образует верхнее сито.

LaTeX

$$$\\text{equalizerSieve } x x = \\top$$$

Lean4

@[simp]
theorem equalizerSieve_self_eq_top {F : Cᵒᵖ ⥤ D} {X : Cᵒᵖ} (x : ToType (F.obj X)) : equalizerSieve x x = ⊤ := by aesop

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

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

Разделы

Аффилиация

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