English
For p, q in the tangent bundle, membership p ∈ chartAt(ModelProd H E) q .target is equivalent to p.1 ∈ chartAt H q.1 .target.
Русский
Для p, q в касательном пространстве принадлежность p к целевой части chartAt(ModelProd H E) q эквивалентна тому, что p.1 принадлежит к цели chartAt H q.1.
LaTeX
$$$p \in (chartAt (ModelProd H E) q).target \;\Longleftrightarrow\; p.1 \in (chartAt H q.1).target$$$
Lean4
@[simp, mfld_simps]
theorem mem_chart_target_iff (p : H × E) (q : TM) :
p ∈ (chartAt (ModelProd H E) q).target ↔ p.1 ∈ (chartAt H q.1).target := by
/- porting note: was
simp +contextual only [FiberBundle.chartedSpace_chartAt,
and_iff_left_iff_imp, mfld_simps]
-/
simp only [FiberBundle.chartedSpace_chartAt, mfld_simps]
rw [PartialEquiv.prod_symm]
simp +contextual only [and_iff_left_iff_imp, mfld_simps]
