piMap

Mathlib.Topology.Constructions

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

← MathLib Explorer

English

The map Quotient.mk' is continuous.

Русский

Картирование Quotient.mk' непрерывно.

LaTeX

$$$$ \mathrm{Continuous}(\operatorname{Quotient.mk'}(X, s)) $$$$

Lean4

@[fun_prop]
protected theorem piMap {f : ∀ i, A i → B i} (hf : ∀ i, Continuous (f i)) : Continuous (Pi.map f) :=
  continuous_pi fun i ↦ (hf i).comp (continuous_apply i)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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