range_eq_ofSection

Mathlib.CategoryTheory.Subpresheaf.OfSection

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

← MathLib Explorer

English

For f: yoneda.obj X ⟶ F, the range of f equals the ofSection corresponding to yonedaEquiv f.

Русский

Для f: yoneda.obj X ⟶ F, диапазон f равен ofSection, соответствующему yonedaEquiv f.

LaTeX

$$$ range\\ f = ofSection (yonedaEquiv.f) $$$

Lean4

theorem range_eq_ofSection {X : C} (f : yoneda.obj X ⟶ F) : range f = ofSection (yonedaEquiv f) := by
  rw [ofSection_eq_range, Equiv.symm_apply_apply]

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

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

Разделы

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

Аффилиация

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