isEmbedding_structureMap — Mathlib

English

The canonical map structureMap from the restricted product to the product is an embedding; the restricted product inherits the subset topology from the ambient product.

Русский

Каноническая карта structureMap ограниченного произведения в произведение является вложением; ограниченное произведение наследует подмножностную топологию из окружающего произведения.

LaTeX

$$$\\text{isEmbedding_structureMap } R A = \\text{IsEmbedding } (\\text{structureMap } R A\\, \\text{cofinite})$$$

Lean4

/-- `Π i, A i` has the subset topology from the restricted product. -/
theorem isEmbedding_structureMap : IsEmbedding (structureMap R A 𝓕) :=
  isEmbedding_inclusion_top.comp homeoTop.isEmbedding

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