fork_π_app_walkingParallelPair_one

Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

URI: https://scilib.ai/kg/mathlib#TopCat.Presheaf.SheafConditionEqualizerProducts.fork_π_app_walkingParallelPair_one

English

Isomorphic presheaves have isomorphic piOpens for any cover U.

Русский

Изоморфные преп presheaf имеют изоморфные piOpens для любого покрытия.

LaTeX

$$$\pi\mathrm{Opens}(F,U) \cong \pi\mathrm{Opens}(G,U)$$$

Lean4

@[simp]
theorem fork_π_app_walkingParallelPair_one : (fork F U).π.app WalkingParallelPair.one = res F U ≫ leftRes F U :=
  rfl

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

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

Разделы

Аффилиация

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