achart_def

Mathlib.Geometry.Manifold.ChartedSpace

URI: https://scilib.ai/kg/mathlib#achart_def

English

Definitional equality for achart: achart(H,x) equals the pair (chartAt(H,x), chart_mem_atlas(H,x)).

Русский

Определительная равенство achart: achart(H,x) совпадает с парой (chartAt(H,x), chart_mem_atlas(H,x)).

LaTeX

$$$\\text{achart}(H,x) = \\langle \\text{chartAt}(H,x), \\text{chart\_mem\_atlas}(H,x) \\rangle$$$

Lean4

theorem achart_def (x : M) : achart H x = ⟨chartAt H x, chart_mem_atlas H x⟩ :=
  rfl

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

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

Разделы

Аффилиация

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