splitLower_eq_self

Mathlib.Analysis.BoxIntegral.Partition.Split

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

English

Simplified lemma: splitLower_eq_bot with the same condition.

Русский

Упрощённая лемма: тот же условие для splitLower_eq_bot.

LaTeX

$$$I.splitLower i x = \\bot \\;\\Leftrightarrow\\; x \\le I.lower i$$$

Lean4

@[simp]
theorem splitLower_eq_self : I.splitLower i x = I ↔ I.upper i ≤ x := by simp [splitLower]

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

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

Разделы

Аффилиация

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