English
Let α be a linearly ordered set and a ∈ α. If f is defined on the ray {y ∈ α | a ≤ y}, and IciExtend is the natural extension of f to all of α, then the value of the extension at x is obtained by evaluating f at max(a, x). Concretely, (IciExtend f)(x) = f(⟨max(a, x), le_max_left(a, x)⟩).
Русский
Пусть α упорядочено линейно, а ∈ α. Пусть f определена на луче {y ∈ α | a ≤ y}. Тогда естественное продолжение IciExtend(f) в точке x равно значению f в точке max(a, x); то есть (IciExtend f)(x) = f(⟨max(a, x), le_max_left(a, x)⟩).
LaTeX
$$$$(IciExtend f)(x) = f\\left\\langle \\max(a,x), \\le\\_\\max\\_left(a,x) \\right\\rangle.$$$$
Lean4
theorem IciExtend_apply (f : Ici a → β) (x : α) : IciExtend f x = f ⟨max a x, le_max_left _ _⟩ :=
rfl
