IccExtend_left

Mathlib.Order.Interval.Set.ProjIcc

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

English

At the left endpoint a, the extended function agrees with f.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem IccExtend_left (f : Icc a b → β) : IccExtend h f a = f ⟨a, left_mem_Icc.2 h⟩ :=
  IccExtend_of_le_left h f le_rfl

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

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

Разделы

Аффилиация

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