sections_ext

Mathlib.Algebra.Category.ModuleCat.Presheaf

URI: https://scilib.ai/kg/mathlib#PresheafOfModules.sections_ext

← MathLib Explorer

English

Two sections are equal if their values are equal at every object.

Русский

Две секции равны, если их значения равны на каждом объекте.

LaTeX

$$$ s = t \;\text{iff}\; \forall X, s.x = t.x $$$

Lean4

@[ext]
theorem sections_ext {M : PresheafOfModules.{v} R} (s t : M.sections) (h : ∀ (X : Cᵒᵖ), s.val X = t.val X) : s = t :=
  Subtype.ext (by ext; apply h)

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

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

Разделы

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

Аффилиация

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