trivialization_mem_atlas — Mathlib

English

For each base point b, the trivialization at b is a member of the atlas of trivializations, i.e., it appears in the collection of trivializations covering the bundle.

Русский

Для каждой базовой точки b тривиализация над b принадлежит атласу тривиализаций фибробандла.

LaTeX

$$$ \operatorname{trivializationAt}(F,E,b)\in \operatorname{trivializationAtlas}(F,E) $$$

Lean4

theorem trivialization_mem_atlas : trivializationAt F E b ∈ trivializationAtlas F E :=
  trivialization_mem_atlas' b

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