presieve₀_singleton

Mathlib.CategoryTheory.Sites.Hypercover.Zero

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

English

The 0-presieve of the singleton arrow f is the singleton presieve on f.

Русский

0-прессивация для одинарного стрелочного отображения f равна единичной презиве на f.

LaTeX

$$(singleton f).presieve_0 = .singleton f$$

Lean4

@[simp]
theorem presieve₀_singleton (f : S ⟶ T) : (singleton f).presieve₀ = .singleton f := by
  simp [singleton, presieve₀, Presieve.ofArrows_pUnit]

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

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

Разделы

Аффилиация

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