intrinsicFrontier_subset

Mathlib.Analysis.Convex.Intrinsic

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

← MathLib Explorer

English

If s is closed, the intrinsic frontier is contained in s.

Русский

Если s замкнуто, внутренняя граница вложена в s.

LaTeX

$$$$ \operatorname{intrinsicFrontier}_{\kappa}(s) \subseteq s \quad\text{(when } s \text{ is closed). } $$$$

Lean4

theorem intrinsicFrontier_subset (hs : IsClosed s) : intrinsicFrontier 𝕜 s ⊆ s :=
  image_subset_iff.2 (hs.preimage continuous_induced_dom).frontier_subset

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

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

Разделы

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

Аффилиация

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