range_subobjectMk_ι

Mathlib.CategoryTheory.Subpresheaf.Subobject

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Subpresheaf.range_subobjectMk_ι

← MathLib Explorer

English

The order isomorphism Subpresheaf F ≃o Subobject F.

Русский

Порядковое изоморфизм Subpresheaf F ≃o Subobject F.

LaTeX

$$$\\mathrm{orderIsoSubobject}\\ F : \\mathrm Subpresheaf F \\cong_o \\mathrm Subobject F$$$

Lean4

@[simp]
theorem range_subobjectMk_ι (A : Subpresheaf F) : range (Subobject.mk A.ι).arrow = A :=
  (((equivalenceMonoOver F).trans (ThinSkeleton.equivalence _).symm).unitIso.app A).to_eq.symm

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

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

Разделы

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

Аффилиация

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