mem_localTriv_target — Mathlib

English

The target of the localTrivAsPartialEquiv i equals the target of the localTriv i.

Русский

Цель локальной тривиализации при i равна целевой части локальной тривиализации как таковой.

LaTeX

$$$(Z.localTrivAsPartialEquiv i).target = (Z.localTriv i).target$$$

Lean4

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

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