intrinsicFrontier_singleton

Mathlib.Analysis.Convex.Intrinsic

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

← MathLib Explorer

English

The intrinsic frontier of a singleton is empty.

Русский

Внутренняя граница множества‑одиночки пуста.

LaTeX

$$$\\operatorname{intrinsicFrontier}_{\\mathbb{k}}(\\{x\\}) = \\varnothing$$$

Lean4

@[simp]
theorem intrinsicFrontier_singleton (x : P) : intrinsicFrontier 𝕜 ({ x } : Set P) = ∅ := by
  rw [intrinsicFrontier, preimage_coe_affineSpan_singleton, frontier_univ, image_empty]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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