prodMk_right

Mathlib.Topology.Constructions.SumProd

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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