obj_surjective_of_im_eq_top

Mathlib.CategoryTheory.Groupoid.Subgroupoid

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Subgroupoid.obj_surjective_of_im_eq_top

← MathLib Explorer

English

If im φ hφ equals top, then φ.obj is surjective.

Русский

Если образ φ равен топу, то отображение объектов φ сюрьективно.

LaTeX

$$$\text{im } φ hφ = \top \Rightarrow Function.Surjective (φ.obj)$$$

Lean4

theorem obj_surjective_of_im_eq_top (hφ : Function.Injective φ.obj) (hφ' : im φ hφ = ⊤) : Function.Surjective φ.obj :=
  by
  rintro d
  rw [← mem_im_objs_iff _ hφ, hφ']
  apply mem_top_objs

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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