top — Mathlib

English

The top morphism property is locally at target with respect to any precoverage that has pullbacks.

Русский

Максимальное свойство морфизмов локально в цели относительно любой предпокрывающей, имеющей pullbacks.

LaTeX

$$$(\top : \text{MorphismProperty } C).IsLocalAtTarget K$$$

Lean4

instance top : IsLocalAtTarget (⊤ : MorphismProperty C) K
    where
  pullbackSnd := by simp
  of_zeroHypercover := by simp

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