splitUpper_eq_bot

Mathlib.Analysis.BoxIntegral.Partition.Split

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

← MathLib Explorer

English

I.splitUpper i x = ⊥ iff I.upper i ≤ x.

Русский

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

LaTeX

$$$I.splitUpper i x = \\bot \\;\\text{ iff }\\; I.upper i \\le x$$$

Lean4

@[simp]
theorem splitUpper_eq_bot {i x} : I.splitUpper i x = ⊥ ↔ I.upper i ≤ x := by
  classical
  rw [splitUpper, mk'_eq_bot, exists_update_iff I.lower fun j y => I.upper j ≤ y]
  simp [(I.lower_lt_upper _).not_ge]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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