sum_chartAt_inr_apply — Mathlib

English

Similarly, for x' ∈ M' and y' ∈ M', we have ((chartAt H (Sum.inr x')).toFun' (Sum.inr y)) = ((chartAt H x').toFun') y.

Русский

Аналогично, для x' ∈ M' и y ∈ M, имеем ((chartAt H (Sum.inr x')).toFun' (Sum.inr y)) = ((chartAt H x').toFun') y.

LaTeX

$$$((chartAt\,H\,(\mathrm{Sum}.\mathrm{inr}\ x')).\mathrm{toFun'}\ (\mathrm{Sum}.\mathrm{inr}\ y)) = ((chartAt\,H\ x').\mathrm{toFun'}\ y).$$$

Lean4

@[simp, mfld_simps]
theorem sum_chartAt_inr_apply {x y : M'} : (chartAt H (.inr x : M ⊕ M')) (Sum.inr y) = (chartAt H x) y :=
  by
  haveI : Nonempty H := nonempty_of_chartedSpace x
  rw [ChartedSpace.sum_chartAt_inr]
  exact OpenPartialHomeomorph.lift_openEmbedding_apply _ _

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