affineCombinationSingleWeights_apply_of_ne

Mathlib.LinearAlgebra.AffineSpace.Combination

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

← MathLib Explorer

English

If i ≠ j, the single weight affine combination at i and j is zero.

Русский

Если i ≠ j, то affineCombinationSingleWeights k i j = 0.

LaTeX

$$$ affineCombinationSingleWeights\ k\ i\ j = 0 \quad \text{if } i \neq j $$$

Lean4

@[simp]
theorem affineCombinationSingleWeights_apply_of_ne [DecidableEq ι] {i j : ι} (h : j ≠ i) :
    affineCombinationSingleWeights k i j = 0 :=
  Pi.single_eq_of_ne h _

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

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

Разделы

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

Аффилиация

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