sieve₀_f

Mathlib.CategoryTheory.Sites.Hypercover.Zero

URI: https://scilib.ai/kg/mathlib#CategoryTheory.PreZeroHypercover.sieve₀_f

English

As above, the zeroth presieve on E.f i is the singleton generated by i.

Русский

Аналогично: нулевое презивное на E.f i — одиночка, порождённая i.

LaTeX

$$$E.presieve_0(E.f(i)) = \langle i \rangle$$$

Lean4

theorem sieve₀_f (i : E.I₀) : E.sieve₀ (E.f i) :=
  ⟨_, 𝟙 _, E.f i, ⟨i⟩, by simp⟩

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

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

Разделы

Аффилиация

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