proj_symm_apply'

Mathlib.Topology.FiberBundle.Trivialization

URI: https://scilib.ai/kg/mathlib#Trivialization.proj_symm_apply'

← MathLib Explorer

English

For b ∈ B and x ∈ F, proj(e.symm(b, x)) = b.

Русский

Для b ∈ B и x ∈ F, proj(e.symm(b,x)) = b.

LaTeX

$$$\mathrm{proj}(e.toOpenPartialHomeomorph.symm {\fst := b, \snd := x}) = b$$$

Lean4

theorem proj_symm_apply' {b : B} {x : F} (hx : b ∈ e.baseSet) : proj (e.toOpenPartialHomeomorph.symm (b, x)) = b :=
  e.toPretrivialization.proj_symm_apply' hx

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

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

Разделы

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

Аффилиация

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