isEmbedding_inclusion_top — Mathlib

English

The inclusion from the restricted product with the top filter (i.e., maximal filter) is an embedding.

Русский

Включение ограниченного произведения при верхнем фильтре (максимальном) является вложением.

LaTeX

$$$\\text{Inclusion } R A (le_{top}: 𝓕 \\le ⊤) \\text{ is an embedding}$$$

Lean4

theorem isEmbedding_inclusion_top : IsEmbedding (inclusion R A (le_top : 𝓕 ≤ ⊤)) :=
  .of_comp (continuous_inclusion _) continuous_coe isEmbedding_coe_of_top

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