exists_mem

Mathlib.Analysis.BoxIntegral.Box.Basic

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

English

The set I.toSet is nonempty.

Русский

Множество I.toSet непусто.

LaTeX

$$$$I.toSet\\;\\neq\\;\\emptyset.$$$$

Lean4

theorem exists_mem : ∃ x, x ∈ I :=
  ⟨_, I.upper_mem⟩

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

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

Разделы

Аффилиация

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