mem_coe

Mathlib.Analysis.BoxIntegral.Box.Basic

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

English

Equivalence of mem_mk under simp.

Русский

Эквивалентность mem_mk в simp.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem mem_coe : x ∈ (I : Set (ι → ℝ)) ↔ x ∈ I :=
  Iff.rfl

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

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

Разделы

Аффилиация

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