sigmaMk

Mathlib.Topology.ContinuousMap.Basic

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

English

For each i ∈ I, the map X_i → Σ_i X_i given by x ↦ (i,x) is continuous.

Русский

Для каждого i ∈ I отображение X_i → Σ_i X_i, x ↦ (i,x), непрерывно.

LaTeX

$$$(\mathrm{Sigma.mk}\ i): X_i \to \Sigma_i X_i \\text{ is continuous } x \mapsto (i,x)$$$

Lean4

/-- `Sigma.mk i` as a bundled continuous map. -/
@[simps apply]
def sigmaMk (i : I) : C(X i, Σ i, X i) where toFun := Sigma.mk i

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

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

Разделы

Аффилиация

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