apply_inl — Mathlib

English

If the i-th index of a line l has the left component a (i.e. idxFun i = Sum.inl a), then the line value at i is a: for any x, l x i = a.

Русский

Если у i-го индекса линии l левая компонента равна a (idxFun i = Sum.inl a), то значение линии на x и i равно a.

LaTeX

$$$\\forall l:\\ Line\\,\\,\\eta\\ to\\ alpha\\,\\iota,\\ \\forall i:\\iota,\\forall a:\\alpha,\\ (l.idxFun\\ i = \\mathrm{Sum.inl}\\,a) \\Rightarrow \\forall x:\\eta\\to\\alpha,\\ l\\,x\\,i = a.$$$

Lean4

theorem apply_inl (h : l.idxFun i = Sum.inl a) : l x i = a := by simp [apply_def, h]

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