maximalAtlas — Mathlib

English

The maximal atlas for a C^n-manifold structure on M is the atlas of all charts compatible with the contDiffGroupoid n I on M.

Русский

Максимальный атлас для структуры C^n-многообразия на M есть атлас всех диаграмм, совместимых с contDiffGroupoid n I на M.

LaTeX

$$$\text{maximalAtlas}(I,n,M) = (\text{contDiffGroupoid}(n,I)).\text{maximalAtlas } M$$$

Lean4

/-- The maximal atlas of `M` for the `C^n` manifold with corners structure corresponding to the
model with corners `I`. -/
def maximalAtlas :=
  (contDiffGroupoid n I).maximalAtlas M

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