instIsIsoOverInferInstanceOverClass

Mathlib.CategoryTheory.Comma.Over.OverClass

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

English

There is an instance asserting that the over cone (S ↓ S) is an isomorphism, derived from identity.

Русский

Существует инстанс, утверждающий, что косина Over (S ↓ S) есть изоморфизм, полученный из тождества.

LaTeX

$$$\mathsf{IsIso}(\mathrm{S}\downarrow \mathrm{S})$$$

Lean4

instance : IsIso (S ↘ S) :=
  inferInstanceAs (IsIso (𝟙 S))

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

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

Разделы

Аффилиация

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