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

∫ Утверждение Mathlib

interUnionPullbackCone_pt

Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

URI: https://scilib.ai/kg/mathlib#TopCat.Sheaf.interUnionPullbackCone_pt

← MathLib Explorer

English

The apex of the pullback cone constructed for the union of opens is precisely F(U ⊔ V).

Русский

Вершина конуса-подпорного для объединения открытий равна F(U ⊔ V).

LaTeX

$$$(\\text{interUnionPullbackCone } F U V).pt = F.1.obj(\\mathrm{op}(U \\cup V))$$$

Lean4

@[simp]
theorem interUnionPullbackCone_pt : (interUnionPullbackCone F U V).pt = F.1.obj (op <| U ⊔ V) :=
  rfl

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

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

Разделы

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

Аффилиация

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

© 2026 SciLib Lab · ФИЦ ИУ РАН. Все права защищены. Контакты: info@scilibai.ru