piMap

Mathlib.Topology.Constructions

URI: https://scilib.ai/kg/mathlib#Topology.IsInducing.piMap

← MathLib Explorer

English

If each f_i is an inducing map, then Pi.map f is inducing.

Русский

Если каждый f_i — индукционный отображение, тогда Pi.map f индуктивен.

LaTeX

$$$$ \mathrm{IsInducing}(\Pi.map f) $$$$

Lean4

protected theorem piMap {f : ∀ i, A i → B i} (hf : ∀ i, IsInducing (f i)) : IsInducing (Pi.map f) := by
  simp [isInducing_iff_nhds, nhds_pi, (hf _).nhds_eq_comap, Filter.pi_comap]

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

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

Разделы

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

Аффилиация

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