compatible_of_mem_maximalAtlas — Mathlib

English

If m ≤ n then maximalAtlas I n M ⊆ maximalAtlas I m M, i.e., larger differentiability level yields a subset relation for maximal atlases when compared from right to left.

Русский

Если m ≤ n, то maximalAtlas I n M ⊆ maximalAtlas I m M, то есть больший уровень дифференцируемости задаёт вложение атласа слева направо.

LaTeX

$$m \le n \Rightarrow maximalAtlas(I,n,M) \subseteq maximalAtlas(I,m,M)$$

Lean4

theorem compatible_of_mem_maximalAtlas {e e' : OpenPartialHomeomorph M H} (he : e ∈ maximalAtlas I n M)
    (he' : e' ∈ maximalAtlas I n M) : e.symm.trans e' ∈ contDiffGroupoid n I :=
  StructureGroupoid.compatible_of_mem_maximalAtlas he he'

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