coe_chartAt_symm_fst — Mathlib

English

A simplified variant of the chart target membership: p ∈ chartAt(ModelProd H E) q .target iff p.1 ∈ chartAt H q.1 .target.

Русский

Упрощенный вариант принадлежности к целевой диаграмме: p ∈ chartAt(ModelProd H E) q .target тогда и только тогда, когда p.1 ∈ chartAt H q.1 .target.

LaTeX

$$$p \in (chartAt (ModelProd H E) q).target \;\Leftrightarrow\; p.1 \in (chartAt H q.1).target$$$

Lean4

@[simp, mfld_simps]
theorem coe_chartAt_symm_fst (p : H × E) (q : TM) :
    ((chartAt (ModelProd H E) q).symm p).1 = ((chartAt H q.1).symm : H → M) p.1 :=
  rfl

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