Nobeling_aux — Mathlib

English

The Nobeling embedding ι is a closed embedding into the space of clopen subsets.

Русский

Встраивание Нёбельинга ι является замкнутым вложением в пространство открытых и замкнутых подмножеств.

LaTeX

$$$IsClosedEmbedding(\\Nobeling.ι S).$$$

Lean4

/-- Given a profinite set `S` and a closed embedding `S → (I → Bool)`, the `ℤ`-module
`LocallyConstant C ℤ` is free.
-/
theorem Nobeling_aux : Module.Free ℤ (LocallyConstant S ℤ) :=
  Module.Free.of_equiv' (Module.Free.of_basis <| GoodProducts.Basis _ hι.isClosed_range)
    (LocallyConstant.congrLeftₗ ℤ hι.isEmbedding.toHomeomorph).symm

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