IciExtend_of_le

Mathlib.Order.Interval.Set.ProjIcc

URI: https://scilib.ai/kg/mathlib#Set.IciExtend_of_le

English

If x is not larger than a, then the extension of f at x equals the endpoint value at a.

Русский

Если x не больше a, то значение расширения f в x равно значению в точке a.

LaTeX

$$$(\\mathrm{IciExtend} f)(x) = f(a) \\quad\\text{если } x \\le a$$$

Lean4

theorem IciExtend_of_le (f : Ici a → β) (hx : x ≤ a) : IciExtend f x = f ⟨a, le_rfl⟩ :=
  congr_arg f <| projIci_of_le hx

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru