mk'_eq_bot

Mathlib.Analysis.BoxIntegral.Box.Basic

URI: https://scilib.ai/kg/mathlib#BoxIntegral.Box.mk'_eq_bot

English

mk' l u equals bottom iff there exists some index i with u_i ≤ l_i.

Русский

mk' l u равно ⊥ тогда, когда существует индекс i с u_i ≤ l_i.

LaTeX

$$$mk'(l,u) = \bot \iff \exists i, u(i) \le l(i)$$$

Lean4

@[simp]
theorem mk'_eq_bot {l u : ι → ℝ} : mk' l u = ⊥ ↔ ∃ i, u i ≤ l i :=
  by
  rw [mk']
  split_ifs with h <;> simpa using h

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

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

Разделы

Аффилиация

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