subset_maximalAtlas — Mathlib

English

The original atlas of M is contained in the maximal atlas for the C^n structure: every chart from atlas H M lies in maximalAtlas I n M.

Русский

Исходный атлас M содержится в максимальном атласе для структуры C^n: каждая диаграмма из атласа H M принадлежит maximalAtlas I n M.

LaTeX

$$atlas(H,M) ⊆ maximalAtlas(I,n,M)$$

Lean4

theorem subset_maximalAtlas [IsManifold I n M] : atlas H M ⊆ maximalAtlas I n M :=
  StructureGroupoid.subset_maximalAtlas _

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