morphismProperty_eq_top — Mathlib

English

If a MorphismProperty P on Paths V contains all identities and is closed under composition with single steps, then P holds for every path; i.e., P is the top element.

Русский

Если свойство морфизмов P над путями Paths V содержит все тождества и замыкается на композиции с одиночными шагами, то оно выполняется для каждого пути; то есть P равно верхнему элементу.

LaTeX

$$$P = \\top$$$

Lean4

/-- A reformulation of `CategoryTheory.Paths.induction` in terms of `MorphismProperty`. -/
theorem morphismProperty_eq_top (P : MorphismProperty (Paths V)) (id : ∀ {v : V}, P (𝟙 ((of V).obj v)))
    (comp : ∀ {u v w : V} (p : (of V).obj u ⟶ (of V).obj v) (q : v ⟶ w), P p → P (p ≫ (of V).map q)) : P = ⊤ :=
  by
  ext; constructor
  · simp
  · exact fun _ ↦ induction (fun f ↦ P f) id comp _

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