prodMk_left

Mathlib.Topology.Constructions.SumProd

URI: https://scilib.ai/kg/mathlib#Continuous.prodMk_left

English

For any fixed y, the map x ↦ (x, y) is continuous.

Русский

Для фиксированного y отображение x ↦ (x, y) непрерывно.

LaTeX

$$$\text{Continuous}(\lambda x, (x,y))$$$

Lean4

@[continuity]
theorem prodMk_left (y : Y) : Continuous fun x : X => (x, y) := by fun_prop

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

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

Разделы

Аффилиация

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