isInducing_prodMkLeft

Mathlib.Topology.Constructions.SumProd

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

English

For a fixed y ∈ Y, the map x ↦ (x, y) is an inducing map from X to X × Y.

Русский

Для фиксированного y ∈ Y отображение x ↦ (x, y) является индуцирующим отображением из X в X × Y.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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