isEmbedding_coe_of_bot — Mathlib

English

The coe map for bot-filtered restricted product is an embedding; the bot version of restricted product has the same embedding property as principal.

Русский

Отображение coe для ограниченного произведения с фильтром ⊥ является вложением; свойство вложенности сохраняется в нулевой форме.

LaTeX

$$IsEmbedding ((↑) : Πʳ i, [R_i, A_i]_[⊥] → Π i, R_i)$$

Lean4

theorem isEmbedding_coe_of_bot : IsEmbedding ((↑) : Πʳ i, [R i, A i]_[⊥] → Π i, R i) :=
  principal_empty ▸ isEmbedding_coe_of_principal

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