mem_def

Mathlib.Analysis.BoxIntegral.Box.Basic

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

English

Same as mem_mk with simp tag.

Русский

То же самое, что mem_mk, с пометкой simp.

LaTeX

$$$$x \\in \\operatorname{mk} l u H \\iff \\forall i, x_i \\in (l_i, u_i].$$$$

Lean4

theorem mem_def : x ∈ I ↔ ∀ i, x i ∈ Ioc (I.lower i) (I.upper i) :=
  Iff.rfl

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

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

Разделы

Аффилиация

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