prod_apply

Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

URI: https://scilib.ai/kg/mathlib#IncidenceAlgebra.prod_apply

English

For any x=(a1,a2) and y=(b1,b2), f.prod g applied to x,y equals f(a1,b1) times g(a2,b2) in the respective coordinates.

Русский

Для любых x=(a1,a2) и y=(b1,b2) f.prod g на x,y равняется f(a1,a2) умножить на g(b1,b2) в соответствующих координатах.

LaTeX

$$$ f.prod g x y = f x.1 y.1 \cdot g x.2 y.2 $$$

Lean4

@[simp]
theorem prod_apply (x y : α × β) : f.prod g x y = f x.1 y.1 * g x.2 y.2 :=
  rfl

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

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

Разделы

Аффилиация

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