prodFun_apply

Mathlib.Analysis.Calculus.Implicit

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

English

For φ an implicit function data, φ.prodFun x = (φ.leftFun x, φ.rightFun x).

Русский

Для заданной функции φ.prodFun x равняется паре значений слева и справа.

LaTeX

$$φ.prodFun x = (φ.leftFun x, φ.rightFun x)$$

Lean4

@[simp]
theorem prodFun_apply (x : E) : φ.prodFun x = (φ.leftFun x, φ.rightFun x) :=
  rfl

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

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

Разделы

Аффилиация

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