coordChange_same

Mathlib.Topology.FiberBundle.Trivialization

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

English

If b ∈ baseSet, then the coordinate change does nothing: e.coordChange e b x = x for all x in F.

Русский

Если b ∈ baseSet, переход координат не меняет значение: e.coordChange e b x = x.

LaTeX

$$$e.coordChange e b x = x$$$

Lean4

theorem coordChange_same (e : Trivialization F proj) {b : B} (h : b ∈ e.baseSet) : e.coordChange e b = id :=
  funext <| e.coordChange_same_apply h

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

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

Разделы

Аффилиация

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