continuous_snd

Mathlib.Topology.Constructions.SumProd

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

English

The projection to the second factor, Prod.snd: X × Y → Y, is continuous.

Русский

Проекция на вторую координату непрерывна.

LaTeX

$$$\\operatorname{Continuous}(\\operatorname{Prod.snd})$$$

Lean4

@[continuity]
theorem continuous_snd : Continuous (@Prod.snd X Y) :=
  (continuous_prodMk.1 continuous_id).2

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

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

Разделы

Аффилиация

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