chartAt_apply

Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra

URI: https://scilib.ai/kg/mathlib#Units.chartAt_apply

English

For units a,b, the chart at a sends b to b (identity in coordinate chart).

Русский

Для единиц $a,b$ карта chartAt на $a$ отправляет $b$ в координатах на месте.

LaTeX

$$For all $a,b\\in R^{\\times}$, $chartAt\_R(a)(b)=b$.$$

Lean4

theorem chartAt_apply {a : Rˣ} {b : Rˣ} : chartAt R a b = b :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru