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