prodFun

Mathlib.Analysis.Calculus.Implicit

URI: https://scilib.ai/kg/mathlib#ImplicitFunctionData.prodFun

English

The product function is defined by x ↦ (leftFun x, rightFun x).

Русский

Произведение функций задается отображением x ↦ (leftFun x, rightFun x).

LaTeX

$$def prodFun (x : E) : F × G := (φ.leftFun x, φ.rightFun x)$$

Lean4

/-- The function given by `x ↦ (leftFun x, rightFun x)`. -/
def prodFun (x : E) : F × G :=
  (φ.leftFun x, φ.rightFun x)

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

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

Разделы

Аффилиация

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