pi_eval

Mathlib.Topology.ContinuousMap.Basic

URI: https://scilib.ai/kg/mathlib#ContinuousMap.pi_eval

English

The evaluation of pi f at a is the function i ↦ f(i)(a). In particular, (pi f) a = (f(i)(a))_i.

Русский

Значение pi f в точке a равно функции i ↦ f(i)(a). В частности, (pi f) a = (f_i(a))_i.

LaTeX

$$$(\pi f) a = \lambda i. f(i) a$$$

Lean4

@[simp]
theorem pi_eval (f : ∀ i, C(A, X i)) (a : A) : (pi f) a = fun i : I => (f i) a :=
  rfl

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

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

Разделы

Аффилиация

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