subset_intrinsicClosure

Mathlib.Analysis.Convex.Intrinsic

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

English

Every subset s is contained in its intrinsic closure.

Русский

Каждое подмножество содержится в своем внутреннем замыкании.

LaTeX

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

Lean4

theorem subset_intrinsicClosure : s ⊆ intrinsicClosure 𝕜 s := fun x hx =>
  ⟨⟨x, subset_affineSpan _ _ hx⟩, subset_closure hx, rfl⟩

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

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

Разделы

Аффилиация

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