subset_maximalAtlas — Mathlib

English

Every element of the atlas belongs to the maximal atlas for any structure groupoid.

Русский

Каждый элемент атласа принадлежит к максимальному атласу для любого структуруированного группоида.

LaTeX

$$$atlas\ H M \subseteq G.maximalAtlas M$ for any $G$ with HasGroupoid M G.$$

Lean4

/-- The elements of the atlas belong to the maximal atlas for any structure groupoid. -/
theorem subset_maximalAtlas [HasGroupoid M G] : atlas H M ⊆ G.maximalAtlas M := fun _ he _ he' ↦
  ⟨G.compatible he he', G.compatible he' he⟩

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