English
The coercion from elemental R x into A is an embedding with closed image, i.e., a closed embedding.
Русский
Каноническое включение элементарного R x в A является вложением с замкнутым образом, то есть замкнутое вложение.
LaTeX
$$IsClosedEmbedding ((↑) : elemental R x → A)$$
Lean4
/-- Construct a term of `ProfiniteGrp` from a type endowed with the structure of a
compact and totally disconnected topological group.
(The condition of being Hausdorff can be omitted here because totally disconnected implies that {1}
is a closed set, thus implying Hausdorff in a topological group.) -/
@[to_additive /-- Construct a term of `ProfiniteAddGrp` from a type endowed with the structure of a
compact and totally disconnected topological additive group.
(The condition of being Hausdorff can be omitted here because totally disconnected implies that {0}
is a closed set, thus implying Hausdorff in a topological additive group.) -/
]
abbrev of (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
[TotallyDisconnectedSpace G] : ProfiniteGrp.{u}
where
toProfinite := .of G
group := ‹_›
topologicalGroup := ‹_›
