mem_localTriv_source — Mathlib

English

A point p in the total space lies in the source of the i-th local trivialization exactly when its base point lies in the i-th base set.

Русский

Точка p в полной области принадлежит источнику i-й локальной тривиализации тогда и только тогда, когда её базовая точка лежит в i-й базовой области.

LaTeX

$$$p \in (Z.localTriv i).source \iff p.1 \in Z.baseSet i$$$

Lean4

@[simp, mfld_simps]
theorem mem_localTriv_source (p : Z.TotalSpace) : p ∈ (Z.localTriv i).source ↔ p.1 ∈ Z.baseSet i :=
  Iff.rfl

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