presieve₀_map

Mathlib.CategoryTheory.Sites.Hypercover.Zero

URI: https://scilib.ai/kg/mathlib#CategoryTheory.PreZeroHypercover.presieve₀_map

English

The presieve₀ commutes with mapping along F: (E.map F).presieve₀ equals E.presieve₀.map F.

Русский

Presieve₀ совместим с отображением; (E.map F).presieve₀ = E.presieve₀.map F.

LaTeX

$$$ (E.map F).presieve₀ = E.presieve₀.map F $$$

Lean4

theorem presieve₀_map : (E.map F).presieve₀ = E.presieve₀.map F :=
  (Presieve.map_ofArrows _).symm

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

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

Разделы

Аффилиация

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