toRange_app_val

Mathlib.CategoryTheory.Subpresheaf.Image

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

English

For any p : F' ⟶ F and i, ((toRange p).app i x).val = p.app i x.

Русский

Для любого p: F' ⟶ F и любого i: ((toRange p).app i x).val = p.app i x.

LaTeX

$$((toRange p).app i x).\text{val} = p.app i x$$

Lean4

theorem toRange_app_val {i : Cᵒᵖ} (x : F'.obj i) : ((toRange p).app i x).val = p.app i x := by simp [toRange]

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

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

Разделы

Аффилиация

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