rangeIcc_apply

Mathlib.Data.DFinsupp.Interval

URI: https://scilib.ai/kg/mathlib#DFinsupp.rangeIcc_apply

English

For any f and g, the i-th Finset component of f.rangeIcc g is Icc(f(i), g(i)).

Русский

Для любых f и g i-я компонента f.rangeIcc g равна Icc(f(i), g(i)).

LaTeX

$$rangeIcc_apply (f g : Π₀ i, α i) (i : ι) : f.rangeIcc g i = Icc (f i) (g i)$$

Lean4

@[simp]
theorem rangeIcc_apply (f g : Π₀ i, α i) (i : ι) : f.rangeIcc g i = Icc (f i) (g i) :=
  rfl

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

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

Разделы

Аффилиация

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