IciExtend_self

Mathlib.Order.Interval.Set.ProjIcc

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

English

Evaluating the extension at the endpoint a yields the original value at a.

Русский

Значение расширения в точке a совпадает с исходным значением в a.

LaTeX

$$$(\\mathrm{IciExtend} f)(a) = f(a)$$$

Lean4

@[simp]
theorem IciExtend_self (f : Ici a → β) : IciExtend f a = f ⟨a, le_rfl⟩ :=
  IciExtend_of_le f le_rfl

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

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

Разделы

Аффилиация

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