initial_isIso_to

Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.initial_isIso_to

English

For any object A and f: A → ⊥, f is an isomorphism.

Русский

Для любого объекта A и f: A → ⊥ изоморфизм.

LaTeX

$$$\\forall A,\\ f: A \\to \\bot_C, \\ IsIso f$$$

Lean4

instance initial_isIso_to {A : C} (f : A ⟶ ⊥_ C) : IsIso f :=
  initialIsInitial.isIso_to _

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

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

Разделы

Аффилиация

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