apply_inr — Mathlib

English

If the i-th index of a line l equals the right component e (idxFun i = Sum.inr e), then the line value at i is given by the value x at e: l x i = x e.

Русский

Если idxFun i = Sum.inr e, то l x i = x e.

LaTeX

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

Lean4

theorem apply_inr (h : l.idxFun i = Sum.inr e) : l x i = x e := by simp [apply_def, h]

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