groupoid_of_isCodetecting_empty

Mathlib.CategoryTheory.Generator.Basic

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

English

If IsCodetecting ∅, then every morphism is an isomorphism.

Русский

Если IsCodetecting(∅), то каждый морфизм является изоморфизмом.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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