lower_le_upper

Mathlib.Analysis.BoxIntegral.Box.Basic

URI: https://scilib.ai/kg/mathlib#BoxIntegral.Box.lower_le_upper

English

For any box I and coordinate i, we have I.lower i ≠ I.upper i.

Русский

Для любой коробки I и координаты i имеем I.lower i ≠ I.upper i.

LaTeX

$$$$I.lower_i \\neq I.upper_i \\quad \\text{для каждого } i,$$$$

Lean4

theorem lower_le_upper : I.lower ≤ I.upper := fun i ↦ (I.lower_lt_upper i).le

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

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

Разделы

Аффилиация

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