restrictLe_apply — Mathlib

English

Restriction acts by simply evaluating at the same index within Iic a.

Русский

Ограничение по величине a просто возвращает то же значение на входе внутри Iic a.

LaTeX

$$$\\forall a:\\,\\alpha,\\ f:(a:\\alpha) \\to \\pi a,\\; \\forall i:\\, Iic(a),\\;\\mathrm{restrictLe}(a)\\ f\\ i = f\\ i$$$

Lean4

@[simp]
theorem restrictLe_apply (a : α) (f : (a : α) → π a) (i : Iic a) : restrictLe a f i = f i :=
  rfl

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