maximalAtlas_mono — Mathlib

English

If G ≤ G' for structure groupoids on H, then the maximal atlas is monotone: G.maximalAtlas M ⊆ G'.maximalAtlas M.

Русский

Если G ≤ G' для структурных группоидов на H, то максимальный атлас монотонен: G.maximalAtlas M ⊆ G'.maximalAtlas M.

LaTeX

$$G \leq G' \Rightarrow G.maximalAtlas M \subseteq G'.maximalAtlas M$$

Lean4

theorem maximalAtlas_mono {G G' : StructureGroupoid H} (h : G ≤ G') : G.maximalAtlas M ⊆ G'.maximalAtlas M :=
  fun _ he e' he' ↦ ⟨h (he e' he').1, h (he e' he').2⟩

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