encodable

Mathlib.Topology.Compactness.SigmaCompact

URI: https://scilib.ai/kg/mathlib#LocallyFinite.encodable

Lean4

/-- If `f : ι → Set X` is a locally finite covering of a σ-compact topological space by nonempty
sets, then the index type `ι` is encodable. -/
protected noncomputable def encodable {ι : Type*} {f : ι → Set X} (hf : LocallyFinite f) (hne : ∀ i, (f i).Nonempty) :
    Encodable ι :=
  @Encodable.ofEquiv _ _ (hf.countable_univ hne).toEncodable (Equiv.Set.univ _).symm

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

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

Разделы

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

Аффилиация

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