lower_le_lower

Mathlib.Analysis.BoxIntegral.Partition.Basic

URI: https://scilib.ai/kg/mathlib#BoxIntegral.Prepartition.lower_le_lower

English

For any J in π, the lower bound of I is ≤ the lower bound of J.

Русский

Для любого J в π нижняя грань I не больше нижней грани J.

LaTeX

$$$I_{\lower} ≤ J_{\lower}$$$

Lean4

theorem lower_le_lower (hJ : J ∈ π) : I.lower ≤ J.lower :=
  Box.antitone_lower (π.le_of_mem hJ)

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

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

Разделы

Аффилиация

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