kuratowskiEmbedding

Mathlib.Topology.MetricSpace.Kuratowski

URI: https://scilib.ai/kg/mathlib#NonemptyCompacts.kuratowskiEmbedding

Lean4

/-- Version of the Kuratowski embedding for nonempty compacts -/
nonrec def kuratowskiEmbedding (α : Type u) [MetricSpace α] [CompactSpace α] [Nonempty α] : NonemptyCompacts ℓ^∞(ℕ)
    where
  carrier := range (kuratowskiEmbedding α)
  isCompact' := isCompact_range (kuratowskiEmbedding.isometry α).continuous
  nonempty' := range_nonempty _

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

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

Разделы

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

Аффилиация

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