fst

Mathlib.Topology.ContinuousMap.Basic

URI: https://scilib.ai/kg/mathlib#ContinuousMap.fst

English

The map fst: α × β → α given by fst(x,y) = x is a continuous map.

Русский

Отображение fst: α × β → α, fst(x,y) = x, является непрерывным отображением.

LaTeX

$$$\text{fst} : C(α \times β, α)$ with toFun := Prod.fst$$

Lean4

/-- `Prod.fst : (x, y) ↦ x` as a bundled continuous map. -/
@[simps -fullyApplied]
def fst : C(α × β, α) where toFun := Prod.fst

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

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

Разделы

Аффилиация

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