productOfMemOpens_isEmbedding — Mathlib

English

In a T0 space, the map productOfMemOpens is an embedding, i.e., it is inducing and injective.

Русский

В T0-пространстве отображение productOfMemOpens является вложением: оно индуцирующее и инъективное.

LaTeX

$$$\text{IsEmbedding}(\text{productOfMemOpens } X).$$$

Lean4

theorem productOfMemOpens_isEmbedding [T0Space X] : IsEmbedding (productOfMemOpens X) :=
  .mk (productOfMemOpens_isInducing X) (productOfMemOpens_injective X)

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