isEmbedding

Mathlib.Topology.DenseEmbedding

URI: https://scilib.ai/kg/mathlib#IsDenseEmbedding.isEmbedding

English

If de is a dense embedding of e, then e is an embedding.

Русский

Если de является плотным вложением e, то e является вложением.

LaTeX

$$$IsDenseEmbedding e \\Rightarrow IsEmbedding e$$$

Lean4

theorem isEmbedding (de : IsDenseEmbedding e) : IsEmbedding e where __ := de

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

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

Разделы

Аффилиация

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