face_mk

Mathlib.Analysis.BoxIntegral.Box.Basic

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

← MathLib Explorer

English

mk' l u equals bottom iff there exists 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 face_mk {n} (l u : Fin (n + 1) → ℝ) (h : ∀ i, l i < u i) (i : Fin (n + 1)) :
    face ⟨l, u, h⟩ i = ⟨l ∘ Fin.succAbove i, u ∘ Fin.succAbove i, fun _ ↦ h _⟩ :=
  rfl

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

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

Разделы

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

Аффилиация

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