groupoid_of_isDetecting_empty

Mathlib.CategoryTheory.Generator.Basic

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

English

If IsDetecting ∅, then every morphism is an isomorphism; the hom-sets form a groupoid.

Русский

Если IsDetecting(∅), то любая стрелка является изоморфизмом; гом-слоя образуют группуoid.

LaTeX

$$$IsDetecting(\emptyset) \Rightarrow (\forall f: X\to Y, IsIso f)$$$

Lean4

theorem groupoid_of_isDetecting_empty (h : IsDetecting (∅ : Set C)) {X Y : C} (f : X ⟶ Y) : IsIso f :=
  h _ fun _ => False.elim

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

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

Разделы

Аффилиация

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