mem_rangeIcc_apply_iff

Mathlib.Data.Finsupp.Interval

URI: https://scilib.ai/kg/mathlib#Finsupp.mem_rangeIcc_apply_iff

English

For all i and a, a ∈ rangeIcc f g at i iff f(i) ≤ a ≤ g(i).

Русский

Для каждого i и a: a в rangeIcc f g на i тогда и только тогда, когда f(i) ≤ a ≤ g(i).

LaTeX

$$$a \\in \\mathrm{rangeIcc}(f,g)(i) \\iff f(i) \\le a \\le g(i)$$$

Lean4

theorem mem_rangeIcc_apply_iff : a ∈ f.rangeIcc g i ↔ f i ≤ a ∧ a ≤ g i :=
  mem_Icc

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

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

Разделы

Аффилиация

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