top_apply

Mathlib.CategoryTheory.MorphismProperty.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.top_apply

English

For any morphism f, the top morphism property holds: (⊤ : MorphismProperty C) f.

Русский

Для любого морфизма f верно свойство верхнего уровня: (⊤ : MorphismProperty C) f.

LaTeX

$$$(\\top : \\mathrm{MorphismProperty}\\; C)\\; f$.$$

Lean4

@[simp]
theorem top_apply {X Y : C} (f : X ⟶ Y) : (⊤ : MorphismProperty C) f := by simp only [top_eq]

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

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

Разделы

Аффилиация

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