IicExtend_apply — Mathlib

English

Let α be linearly ordered and b ∈ α. If f is defined on the ray {y ∈ α | y ≤ b}, and IicExtend is the natural extension of f to all of α, then the value at x is f evaluated at min(b, x). Concretely, (IicExtend f)(x) = f(⟨min(b, x), min_le_left(b, x)⟩).

Русский

Пусть α упорядочено линейно и b ∈ α. Пусть f определена на луче {y ∈ α | y ≤ b}. Тогда расширение IicExtend(f) в точке x равно значению f в точке min(b, x).

LaTeX

$$$$(IicExtend f)(x) = f\\left\\langle \\min(b,x), \\min\\_\\le\\_left(b,x)\\right\\rangle.$$$$

Lean4

theorem IicExtend_apply (f : Iic b → β) (x : α) : IicExtend f x = f ⟨min b x, min_le_left _ _⟩ :=
  rfl

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