continuous_proj

Mathlib.Topology.FiberBundle.Constructions

URI: https://scilib.ai/kg/mathlib#Pullback.continuous_proj

← MathLib Explorer

English

The projection map π to the base is continuous for pullback total spaces.

Русский

Проекция на основание непрерывна для пространств общей вытяжки.

LaTeX

$$$\mathrm{Continuous}\,\pi_{F(f\cdot^{p}E)}$$$

Lean4

theorem continuous_proj (f : B' → B) : Continuous (π F(f *ᵖ E)) :=
  by
  rw [continuous_iff_le_induced, Pullback.TotalSpace.topologicalSpace, pullbackTopology_def]
  exact inf_le_left

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

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

Разделы

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

Аффилиация

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