mem_chart_source_iff — Mathlib

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]

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