fork_π_app_walkingParallelPair_zero

Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

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

English

If F ≅ G, then piInters F U ≅ piInters G U, compatibly in each coordinate.

Русский

Если F ≅ G, то piInters F U ≅ piInters G U, согласовано по координатам.

LaTeX

$$$\pi\mathrm{Inters}(F,U) \cong \pi\mathrm{Inters}(G,U)\quad\text{via }\Pi\mapsto\text{iso}$$$

Lean4

@[simp]
theorem fork_π_app_walkingParallelPair_zero : (fork F U).π.app WalkingParallelPair.zero = res F U :=
  rfl

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

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

Разделы

Аффилиация

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