English
For p, q in the tangent bundle, membership p ∈ chartAt(ModelProd H E) q .source is equivalent to p.1 ∈ chartAt H q.1 .source.
Русский
Для точек p, q в касательном пространстве принадлежность p к источнику chartAt(ModelProd H E) q эквивалентна принадлежности p.1 к источнику chartAt H q.1.
LaTeX
$$$p \in (chartAt (ModelProd H E) q).source \;\Longleftrightarrow\; p.1 \in (chartAt H q.1).source$$$
Lean4
@[simp, mfld_simps]
theorem mem_chart_source_iff (p q : TM) : p ∈ (chartAt (ModelProd H E) q).source ↔ p.1 ∈ (chartAt H q.1).source := by
simp only [FiberBundle.chartedSpace_chartAt, mfld_simps]