affineCombinationSingleWeights_apply_self

Mathlib.LinearAlgebra.AffineSpace.Combination

URI: https://scilib.ai/kg/mathlib#Finset.affineCombinationSingleWeights_apply_self

← MathLib Explorer

English

For any i, affineCombinationSingleWeights k i i equals 1.

Русский

Для любого i аффинная комбинация единичных весов по i и i равна единице.

LaTeX

$$$$ affineCombinationSingleWeights\; k\; i\; i = 1. $$$$

Lean4

@[simp]
theorem affineCombinationSingleWeights_apply_self [DecidableEq ι] (i : ι) : affineCombinationSingleWeights k i i = 1 :=
  Pi.single_eq_same _ _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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