intrinsicFrontier_subset_intrinsicClosure

Mathlib.Analysis.Convex.Intrinsic

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

English

The intrinsic frontier is contained in the intrinsic closure.

Русский

Граница внутренности содержится в её внутреннем замыкании.

LaTeX

$$$$ \operatorname{intrinsicFrontier}_{\kappa}(s) \subseteq \operatorname{intrinsicClosure}_{\kappa}(s). $$$$

Lean4

theorem intrinsicFrontier_subset_intrinsicClosure : intrinsicFrontier 𝕜 s ⊆ intrinsicClosure 𝕜 s :=
  image_mono frontier_subset_closure

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

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

Разделы

Аффилиация

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