mem_localTrivAsPartialEquiv_target

English

For every p in the total space, p lies in the target of the i-th local trivialization exactly when its first coordinate (the base point) lies in baseSet i.

Русский

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

LaTeX

$$$p \\in \\mathrm{tgt}(\\mathcal{L}_i) \\iff p.1 \\in \\mathrm{baseSet}\\,i$$$

Lean4

theorem mem_localTrivAsPartialEquiv_target (p : B × F) : p ∈ (Z.localTrivAsPartialEquiv i).target ↔ p.1 ∈ Z.baseSet i :=
  by
  rw [localTrivAsPartialEquiv, mem_prod]
  simp only [and_true, mem_univ]

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