functorPullback_top — Mathlib

English

For any functor F and object X, the pullback of the top sieve along F is still top: (⊤ : Sieve (F.obj X)).functorPullback F = ⊤.

Русский

Для любого функторa F и объекта X — обратное изображение верхней щели по F остается верхней щелью.

LaTeX

$$$(\\top : Sieve (F.obj X)).functorPullback F = \\top$$$

Lean4

@[simp]
theorem functorPullback_top (F : C ⥤ D) (X : C) : (⊤ : Sieve (F.obj X)).functorPullback F = ⊤ :=
  rfl

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