instMemTrivializationAtlasTrivializationAt

English

There is a canonical instance stating that for every base point b, the trivialization at b belongs to the atlas of trivializations.

Русский

Существует каноническое утверждение: для каждого b тривиализация над b принадлежит атласу тривиализаций.

LaTeX

$$⟨trivializationAt(F,E,b)∈trivializationAtlas(F,E)⟩$$

Lean4

instance [FiberBundle F E] (b : B) : MemTrivializationAtlas (trivializationAt F E b) where
  out := trivialization_mem_atlas F E b

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