monotone_eval — Mathlib

English

For any i in a family of preordered types α(i), the evaluation map at i is monotone.

Русский

Для любого i из семейства типов α(i) с предуровнями, отображение оценки в i монотонно.

LaTeX

$$$\\forall i,\\mathrm{Monotone}(\\mathrm{Function.eval}_i)$$$

Lean4

theorem monotone_eval {ι : Type u} {α : ι → Type v} [∀ i, Preorder (α i)] (i : ι) :
    Monotone (Function.eval i : (∀ i, α i) → α i) := fun _ _ H ↦ H i

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