coe_eq_pi

Mathlib.Analysis.BoxIntegral.Box.Basic

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

English

I.toSet equals the product univ of Ioc intervals.

Русский

I.toSet равняется произведению универсума интервалов Ioc.

LaTeX

$$$$I^{toSet} = (\\text{univ} \\; \\pi i \\mapsto (I.lower i, I.upper i] ).$$$$

Lean4

theorem coe_eq_pi : (I : Set (ι → ℝ)) = pi univ fun i ↦ Ioc (I.lower i) (I.upper i) :=
  Set.ext fun _ ↦ mem_univ_Ioc.symm

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

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

Разделы

Аффилиация

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