toRange_app_val

Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

URI: https://scilib.ai/kg/mathlib#SSet.Subcomplex.toRange_app_val

English

For any Δ, the value of the Range of f at Δ applied to x equals f's value at Δ and x.

Русский

Для любого Δ, значение (toRange f).app Δ x равно значению f.app Δ x.

LaTeX

$$$$ ((toRange f).app \Delta x).val = f.app \Delta x $$$$

Lean4

@[simp]
theorem toRange_app_val {Δ : SimplexCategoryᵒᵖ} (x : X.obj Δ) : ((toRange f).app Δ x).val = f.app Δ x :=
  rfl

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

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

Разделы

Аффилиация

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