split_apply — Mathlib

English

For a finitely supported function l on the sigma-type Σ i, αs i, and an index i with a corresponding element x, the value of l.split i at x equals l(⟨i, x⟩).

Русский

Пусть l : (Σ i, αs i) →₀ M. Тогда для индекса i и элемента x значение l.split i на x равно l(⟨i, x⟩).

LaTeX

$$$\\mathrm{split}\\; l\\; i\\; x = l\\,\\langle i, x \\rangle$$$

Lean4

theorem split_apply (i : ι) (x : αs i) : split l i x = l ⟨i, x⟩ := by rw [split, comapDomain_apply]

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