partialSups_le

Mathlib.Order.PartialSups

URI: https://scilib.ai/kg/mathlib#partialSups_le

English

If for all j ≤ i we have f(j) ≤ a, then partialSups f i ≤ a.

Русский

Если для всех j ≤ i выполняется f(j) ≤ a, то partialSups f i ≤ a.

LaTeX

$$$\\forall j \\le i,\\; f(j) \\le a \\quad\\Rightarrow\\quad \\mathrm{partialSups} f(i) \\le a$$$

Lean4

theorem partialSups_le (f : ι → α) (i : ι) (a : α) (w : ∀ j ≤ i, f j ≤ a) : partialSups f i ≤ a :=
  partialSups_le_iff.2 w

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

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

Разделы

Аффилиация

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