continuous_fst

Mathlib.Topology.Constructions.SumProd

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

English

The projection to the first factor, Prod.fst: X × Y → X, is a continuous map.

Русский

Проекция на первую координату, Prod.fst: X × Y → X, непрерывна.

LaTeX

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

Lean4

@[continuity]
theorem continuous_fst : Continuous (@Prod.fst X Y) :=
  (continuous_prodMk.1 continuous_id).1

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

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

Разделы

Аффилиация

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