mem_localTriv_target — Mathlib

English

A point p belongs to the target 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).target \iff p.1 \in (Z.localTriv i).baseSet$$$

Lean4

@[simp, mfld_simps]
theorem mem_localTriv_target (p : B × F) : p ∈ (Z.localTriv i).target ↔ p.1 ∈ (Z.localTriv i).baseSet :=
  Z.toFiberBundleCore.mem_localTriv_target i p

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