isExposed_empty

Mathlib.Analysis.Convex.Exposed

URI: https://scilib.ai/kg/mathlib#isExposed_empty

English

The empty set is exposed with respect to any set A.

Русский

Пустое множество экспонировано относительно любого множества A.

LaTeX

$$$\\mathrm{IsExposed}\\ 𝕜\\ A\\ ∅$$$

Lean4

theorem isExposed_empty : IsExposed 𝕜 A ∅ := fun ⟨_, hx⟩ =>
  by
  exfalso
  exact hx

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

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

Разделы

Аффилиация

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