splitUpper_eq_self

Mathlib.Analysis.BoxIntegral.Partition.Split

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

English

I.splitUpper i x = I iff x ≤ I.lower i.

Русский

I.splitUpper i x = I тогда и только тогда, когда x ≤ I.lower i.

LaTeX

$$$I.splitUpper i x = I \\;\\Leftrightarrow\\; x \\le I.lower i$$$

Lean4

@[simp]
theorem splitUpper_eq_self : I.splitUpper i x = I ↔ x ≤ I.lower i := by simp [splitUpper]

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

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

Разделы

Аффилиация

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