toSubspace_apply — Mathlib

English

For l: Line (η → α) ι, x, i, the value of (toSubspace l).toFun x at i is given by evaluating l on the η-component of x at i.

Русский

Для линии l: Line (η → α) ι значение (toSubspace l).toFun x в i равно значению l на η-компоненте x на i.

LaTeX

$$$(\\mathrm{toSubspace} l).toFun x i = \\mathrm{toFun}(l)(\\mathrm{Function.ofComp}(x, \\mathrm{η}))\\big(i\\big)$$$

Lean4

@[simp]
theorem toSubspace_apply (l : Line (η → α) ι) (a ie) : ⇑l.toSubspace a ie = l a ie.1 ie.2 := by
  cases h : l.idxFun ie.1 <;> simp [toSubspace, h, coe_apply, Subspace.coe_apply]

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