inter_def

Mathlib.CategoryTheory.Sites.Hypercover.Zero

URI: https://scilib.ai/kg/mathlib#CategoryTheory.PreZeroHypercover.inter_def

← MathLib Explorer

English

Equivalence-based restriction leaves the zeroth presieve unchanged.

Русский

Ограничение по эквивалентности не изменяет нулевое презивное.

LaTeX

$$(E.restrictIndex (EquivLike.toFunLike.coe e)).presieve₀ = E.presieve₀$$

Lean4

theorem inter_def [∀ i j, HasPullback (E.f i) (F.f j)] :
    E.inter F = (E.bind (fun i ↦ F.pullback₁ (E.f i))).reindex (Equiv.sigmaEquivProd _ _).symm :=
  rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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