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 ⋙ uliftFunctor ⟶ F, the range of f equals ofSection (uliftYonedaEquiv f).

Русский

Для f: yoneda.obj X ⋙ uliftFunctor ⟶ F, диапазон f равен ofSection (uliftYonedaEquiv f).

LaTeX

$$$ range\\ f = ofSection (uliftYonedaEquiv f) $$$

Lean4

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

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

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

Разделы

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

Аффилиация

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