bot_arrow

Mathlib.CategoryTheory.Subobject.Lattice

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Subobject.bot_arrow

English

The arrow of the bottom subobject is the zero morphism.

Русский

Стрела нижнего подмножества равна нулевому морфизму.

LaTeX

$$$ (\\bot : Subobject B).arrow = 0 $$$

Lean4

@[simp]
theorem bot_arrow {B : C} : (⊥ : Subobject B).arrow = 0 :=
  zero_of_source_iso_zero _ botCoeIsoZero

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru