functorPullback_bot — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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