instMemTrivializationAtlasTrivializationOfMemPretrivializationAtlas

English

There is an instance that ensures MemTrivializationAtlas for each pretrivialization in the atlas.

Русский

Существует экземпляр, обеспечивающий MemTrivializationAtlas для каждой предтривиализации в атласе.

LaTeX

$$$ \text{instMemTrivializationAtlasTrivializationOfMemPretrivializationAtlas }(a) $$$

Lean4

instance {e₀} (he₀ : e₀ ∈ a.pretrivializationAtlas) :
    (letI := a.totalSpaceTopology;
    letI := a.toFiberBundle
    MemTrivializationAtlas (a.trivializationOfMemPretrivializationAtlas he₀)) :=
  letI := a.totalSpaceTopology;
  letI := a.toFiberBundle;
  ⟨e₀, he₀, rfl⟩

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