leInfCone_π_app_none — Mathlib

English

The projection component at the initial object (none) of the cone coincides with the apex arrow f.arrow.

Русский

Компонента проекции конуса на нулевой (none) индекс совпадает с стрелкой вершины f.arrow.

LaTeX

$$ (leInfCone s f k).π.app none = f.arrow$$

Lean4

@[simp]
theorem leInfCone_π_app_none {A : C} (s : Set (Subobject A)) (f : Subobject A) (k : ∀ g ∈ s, f ≤ g) :
    (leInfCone s f k).π.app none = f.arrow :=
  rfl

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