chartAt_source

Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra

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

English

The source of the chart at any unit a is the whole space (Set.univ).

Русский

Источник карты chartAt для любой единицы равен всему пространству.

LaTeX

$$For any $a\in R^{\times}$, $(chartAt\,R\,a).source = \mathrm{Set.univ}$.$$

Lean4

theorem chartAt_source {a : Rˣ} : (chartAt R a).source = Set.univ :=
  rfl

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

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

Разделы

Аффилиация

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