coe_ne_empty

Mathlib.Analysis.BoxIntegral.Box.Basic

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

English

Let I be a box in ι. Then the underlying set of points in I is nonempty.

Русский

Пусть I — коробка в ι. Тогда множество точек, принадлежащих I, непусто.

LaTeX

$$$ (I : Set (ι \\to ℝ)) \\neq \\emptyset $$$

Lean4

@[simp]
theorem coe_ne_empty : (I : Set (ι → ℝ)) ≠ ∅ :=
  I.nonempty_coe.ne_empty

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

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

Разделы

Аффилиация

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