inner_eq_ite

Mathlib.Analysis.InnerProductSpace.PiL2

URI: https://scilib.ai/kg/mathlib#OrthonormalBasis.inner_eq_ite

← MathLib Explorer

English

The inner product between b i and b j equals 1 if i=j and 0 otherwise.

Русский

Скалярное произведение b_i и b_j равно 1, если i=j, и 0 иначе.

LaTeX

$$⟪b i, b j⟫ = if i = j then 1 else 0$$

Lean4

theorem inner_eq_ite [DecidableEq ι] (b : OrthonormalBasis ι 𝕜 E) (i j : ι) : ⟪b i, b j⟫ = if i = j then 1 else 0 := by
  by_cases h : i = j <;> simp [h]

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

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

Разделы

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

Аффилиация

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