mem_localTrivAsPartialEquiv_source

English

For every p in the total space and index i, p lies in the source of the i-th local trivialization exactly when its base projection p.proj lies in baseSet i.

Русский

Для любого элемента p из полного пространства и индекса i верно: p принадлежит источнику i-й локальной тривиализации тогда и только тогда, когда проекция p на основание принадлежит baseSet i.

LaTeX

$$$p \\in \\mathrm{src}(\\mathcal{L}_i) \\iff p.\\text{proj} \\in \\mathrm{baseSet}\\,i$$$

Lean4

theorem mem_localTrivAsPartialEquiv_source (p : Z.TotalSpace) :
    p ∈ (Z.localTrivAsPartialEquiv i).source ↔ p.1 ∈ Z.baseSet i :=
  Iff.rfl

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