coe_mem_source

Mathlib.Topology.FiberBundle.Trivialization

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

English

Applying the composed trivialization to a point yields the expected coordinates.

Русский

Применение скомпонованной тривиализации к точке даёт ожидаемые координаты.

LaTeX

$$$ (e.compHomeomorph h) p = ? $$$

Lean4

theorem coe_mem_source : ↑y ∈ e'.source ↔ b ∈ e'.baseSet :=
  e'.mem_source

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

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

Разделы

Аффилиация

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