English
Let α be linearly ordered and a ≤ b. If f is defined on the closed interval Icc(a, b) and IccExtend is its extension to α, then the value at x is f evaluated at the point max(a, min(b, x)) in the interval, with the appropriate endpoint proofs. Concretely, (IccExtend h f x) = f(⟨max(a, min(b, x)), le_max_left(a, min(b,x)), max_le(h)(min(b,x))⟩).
Русский
Пусть α упорядочено линейно и a ≤ b. Пусть f определена на замкнутый отрезок Icc(a,b). Тогда расширение IccExtend(h, f) в точке x равно значению f в точке max(a, min(b, x)) внутри отрезка.
LaTeX
$$$$ IccExtend\_h f x = f\\left\\langle \\max\\left(a,\\min\\left(b,x\\right)\\right), \\le\\_\\max\\_left(a,\\min\\_b\\_x), \\max\\_le\\_h\\left(a,\\min\\_b\\_x\\right)\\rangle \\right.$$$$
Lean4
theorem IccExtend_apply (h : a ≤ b) (f : Icc a b → β) (x : α) :
IccExtend h f x = f ⟨max a (min b x), le_max_left _ _, max_le h (min_le_left _ _)⟩ :=
rfl
