continuousOn_proj

Mathlib.Topology.FiberBundle.Trivialization

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

English

Apply the symmetric of the preimageHomeomorph to a pair (b, y).

Русский

Применение симметрического гомеоморфизма к паре (b, y).

LaTeX

$$$ (e.preimageHomeomorph hb).symm p = (e.symm (p.1, p.2), ((preimageHomeomorph_symm_apply.aux e hb) p).2) $$$

Lean4

theorem continuousOn_proj : ContinuousOn proj e.source :=
  continuousOn_of_forall_continuousAt fun _ ↦ e.continuousAt_proj

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

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

Разделы

Аффилиация

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