inl

Mathlib.Topology.Instances.TrivSqZeroExt

URI: https://scilib.ai/kg/mathlib#TrivSqZeroExt.IsEmbedding.inl

English

The map inl: R → tsze R M is an embedding.

Русский

Отображение inl: R → tsze R M является вложением (embedding).

LaTeX

$$$\\mathrm{IsEmbedding}(\\mathrm{inl}).$$$

Lean4

theorem inl [Zero M] : IsEmbedding (inl : R → tsze R M) :=
  .of_comp continuous_inl continuous_fst .id

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru