isEmbedding_coe_of_principal — Mathlib

English

If all R_i are T0, T1, T2 etc., the coe map gives an embedding; thus the restricted product inherits separation properties.

Русский

Если все R_i удовлетворяют T0, T1, T2, то отображение coe задаёт вложение, и ограниченное произведение наследует разделительные свойства.

LaTeX

$$IsEmbedding (coe) when each R_i has separation properties.$$

Lean4

theorem isEmbedding_coe_of_principal : IsEmbedding ((↑) : Πʳ i, [R i, A i]_[𝓟 S] → Π i, R i)
    where
  eq_induced := topologicalSpace_eq_of_principal
  injective := DFunLike.coe_injective

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