weightedVSubVSubWeights_apply_left

Mathlib.LinearAlgebra.AffineSpace.Combination

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

← MathLib Explorer

English

Alternative statement of left-one property for weights when i ≠ j.

Русский

Альтернативное утверждение о левой единице весов при i ≠ j.

LaTeX

$$$ weightedVSubVSubWeights\ k i j i = 1 $ if $ i \neq j $$$

Lean4

@[simp]
theorem weightedVSubVSubWeights_apply_left [DecidableEq ι] {i j : ι} (h : i ≠ j) :
    weightedVSubVSubWeights k i j i = 1 := by simp [weightedVSubVSubWeights, h]

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

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

Разделы

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

Аффилиация

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