face_mono

Mathlib.Analysis.BoxIntegral.Box.Basic

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

← MathLib Explorer

English

mk' l u equals I iff corners match: l = I.lower and u = I.upper.

Русский

mk' l u равно I тогда, когда углы совпадают: l = I.lower и u = I.upper.

LaTeX

$$$mk' (l,u) = I \iff (l = I.lower) \land (u = I.upper)$$$

Lean4

@[gcongr, mono]
theorem face_mono {n} {I J : Box (Fin (n + 1))} (h : I ≤ J) (i : Fin (n + 1)) : face I i ≤ face J i := fun _ hx _ ↦
  Ioc_subset_Ioc ((le_iff_bounds.1 h).1 _) ((le_iff_bounds.1 h).2 _) (hx _)

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

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

Разделы

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

Аффилиация

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