isEmbedding_prodMkLeft

Mathlib.Topology.Constructions.SumProd

URI: https://scilib.ai/kg/mathlib#isEmbedding_prodMkLeft

English

For every y ∈ Y, the map x ↦ (x, y) is an embedding.

Русский

Для каждого y ∈ Y отображение x ↦ (x, y) является вложением.

LaTeX

$$$\IsEmbedding(\lambda x: X, (x, y))$$$

Lean4

theorem isEmbedding_prodMkLeft (y : Y) : IsEmbedding (fun x : X ↦ (x, y)) :=
  .of_comp (.prodMk_left y) continuous_fst .id

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

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

Разделы

Аффилиация

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