IccExtend_right

Mathlib.Order.Interval.Set.ProjIcc

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

English

At the right endpoint b, the extended function matches f at b.

Русский

На правом краю b расширенная функция совпадает с f в b.

LaTeX

$$$(\\mathrm{IccExtend} h f)(b) = f(b)$$$

Lean4

@[simp]
theorem IccExtend_right (f : Icc a b → β) : IccExtend h f b = f ⟨b, right_mem_Icc.2 h⟩ :=
  IccExtend_of_right_le h f le_rfl

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

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

Разделы

Аффилиация

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