mk_proj_snd'

Mathlib.Topology.FiberBundle.Trivialization

URI: https://scilib.ai/kg/mathlib#Pretrivialization.mk_proj_snd'

English

If proj(x) ∈ e.baseSet, then (proj x, (e x).2) = e(x).

Русский

Если proj(x) ∈ e.baseSet, то (proj x, (e x).2) = e(x).

LaTeX

$$$(\mathrm{proj}(x), (e(x)).2) = e(x) \quad \text{при } \mathrm{proj}(x) \in e.baseSet$$$

Lean4

theorem mk_proj_snd' (ex : proj x ∈ e.baseSet) : (proj x, (e x).2) = e x :=
  Prod.ext (e.coe_fst' ex).symm rfl

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

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

Разделы

Аффилиация

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