sieve₀_trivial

Mathlib.CategoryTheory.Sites.Hypercover.One

URI: https://scilib.ai/kg/mathlib#CategoryTheory.PreOneHypercover.sieve₀_trivial

English

Top sieve for trivial presheaf on S is top.

Русский

Верхний sieve для тривиального префункторa над S — верх.

LaTeX

$$$ (trivial S).sieve_0 = \\top $$$

Lean4

theorem sieve₀_trivial (S : C) : (trivial S).sieve₀ = ⊤ :=
  by
  rw [PreZeroHypercover.sieve₀, Sieve.ofArrows, ← PreZeroHypercover.presieve₀]
  simp

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

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

Разделы

Аффилиация

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