hasCardinalLT_of_mono

Mathlib.CategoryTheory.Subobject.HasCardinalLT

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Subobject.hasCardinalLT_of_mono

← MathLib Explorer

English

For a morphism f, IsIso f is equivalent to Subobject.mk f = ⊤.

Русский

Для морфизма f эквивалентно IsIso f = Subobject.mk f = ⊤.

LaTeX

$$$\text{IsIso } f \iff \operatorname{Subobject}.mk f = \top$$$

Lean4

theorem hasCardinalLT_of_mono {Y : C} {κ : Cardinal.{w}} (h : HasCardinalLT (Subobject Y) κ) {X : C} (f : X ⟶ Y)
    [Mono f] : HasCardinalLT (Subobject X) κ :=
  h.of_injective _ (map_obj_injective f)

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

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

Разделы

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

Аффилиация

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