antitone_lower

Mathlib.Analysis.BoxIntegral.Box.Basic

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

English

If I ≤ J then I.lower ≥ J.lower.

Русский

Если I ≤ J, то I.lower ≥ J.lower.

LaTeX

$$$ I \\le J \\Rightarrow I.lower \\ge J.lower $$$

Lean4

theorem antitone_lower : Antitone fun I : Box ι ↦ I.lower := fun _ _ H ↦ (le_iff_bounds.1 H).1

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

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

Разделы

Аффилиация

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