botCoeIsoInitial — Mathlib

English

The object underlying ⊥ : Subobject B is (up to isomorphism) the initial object of the category.

Русский

Объект, лежащий в основе ⊥ : Subobject B, изоморфен начальному объекту категории.

LaTeX

$$$ ((\\bot : Subobject B) : C) \\cong 0 $$$

Lean4

/-- The object underlying `⊥ : Subobject B` is (up to isomorphism) the initial object. -/
def botCoeIsoInitial {B : C} : ((⊥ : Subobject B) : C) ≅ ⊥_ C :=
  underlyingIso _

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