isEmbedding_inclusion_principal — Mathlib

English

For S with cofinite relation, the inclusion map from the restricted product into the full product is an embedding.

Русский

При S с кофинитной связью включение из ограниченного произведения в полное произведение является вложением (эмбеддингом).

LaTeX

$$$\\text{Inclusion } R A hS: \\text{IsEmbedding}$$$

Lean4

theorem isEmbedding_inclusion_principal {S : Set ι} (hS : 𝓕 ≤ 𝓟 S) : IsEmbedding (inclusion R A hS) :=
  .of_comp (continuous_inclusion hS) continuous_coe isEmbedding_coe_of_principal

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