ι — Mathlib · SciLib

English

The canonical embedding of a profinite S into the Boolean function space given by clopen subsets is an injective topological embedding.

Русский

Каноническое вложение профинитивного множества S в пространство булевых функций по открытым множествам является инъективным топологическим вложением.

LaTeX

$$$ι: S \\to (I \\to Bool)$ is an embedding with closed image.$$

Lean4

/-- The embedding `S → (I → Bool)` where `I` is the set of clopens of `S`. -/
noncomputable def ι : S → ({ C : Set S // IsClopen C } → Bool) := fun s C => decide (s ∈ C.1)

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