sieve₁_trivial

Mathlib.CategoryTheory.Sites.Hypercover.One

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

English

Top sieve1 for trivial presheaf.

Русский

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

LaTeX

$$$ (trivial S).sieve_1 p p = \\top $$$

Lean4

@[simp]
theorem sieve₁_trivial {S : C} {W : C} {p : W ⟶ S} : (trivial S).sieve₁ (i₁ := ⟨⟩) (i₂ := ⟨⟩) p p = ⊤ := by ext; simp

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

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

Разделы

Аффилиация

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