inj_iff

Mathlib.Topology.DenseEmbedding

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

English

If de1 : IsDenseEmbedding e1 and de2 : IsDenseEmbedding e2, then the map p ↦ (e1 p1, e2 p2) is a dense embedding.

Русский

Если имеются плотные вложения e1 и e2, то отображение p ↦ (e1 p1, e2 p2) является плотным вложением.

LaTeX

$$$IsDenseEmbedding (fun p => (e_1 p.1, e_2 p.2))$$$

Lean4

theorem inj_iff (de : IsDenseEmbedding e) {x y} : e x = e y ↔ x = y :=
  de.injective.eq_iff

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

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

Разделы

Аффилиация

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