continuousAt_proj

Mathlib.Topology.FiberBundle.Trivialization

URI: https://scilib.ai/kg/mathlib#Trivialization.continuousAt_proj

← MathLib Explorer

English

Apply the preimageHomeomorph to an element of the preimage.

Русский

Применение предобразного гомоморфизма к элементу предобраза.

LaTeX

$$$ e.preimageHomeomorph_apply hb p = (\langle proj p, p.2 \rangle, (e p).2) $$$

Lean4

/-- In the domain of a bundle trivialization, the projection is continuous -/
theorem continuousAt_proj (ex : x ∈ e.source) : ContinuousAt proj x :=
  (e.map_proj_nhds ex).le

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

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

Разделы

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

Аффилиация

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