instIsOverTower_1

Mathlib.CategoryTheory.Comma.Over.OverClass

URI: https://scilib.ai/kg/mathlib#CategoryTheory.instIsOverTower_1

English

If X is over S, then IsOverTower X S S holds.

Русский

Если X над S, то выполняется IsOverTower X S S.

LaTeX

$$$\forall {\mathcal C} \ [\text{Category}(\mathcal C)], \ X \in \mathcal C, \ [OverClass X S] \Rightarrow \ IsOverTower\ X\ S\ S$$

Lean4

instance [OverClass X S] : IsOverTower X S S where

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

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

Разделы

Аффилиация

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