splitLower_eq_bot

Mathlib.Analysis.BoxIntegral.Partition.Split

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

← MathLib Explorer

English

I.splitLower i x = ⊥ iff x ≤ I.lower i.

Русский

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

LaTeX

$$$I.splitLower i x = \\bot \\;\\text{ iff }\\; x \\le I.lower i$$$

Lean4

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

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

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

Разделы

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

Аффилиация

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