hasGroupoid_model_space — Mathlib

English

The trivial charted-space structure on the model space is compatible with any groupoid.

Русский

Общая (тривиальная) структура чартизованного пространства на модельном пространстве совместима с любым групоидом.

LaTeX

$$$HasGroupoid\ H\ G\;\text{for any } G\text{, with the model-space chart} \text{space.}$$$

Lean4

/-- The trivial charted space structure on the model space is compatible with any groupoid. -/
instance hasGroupoid_model_space (H : Type*) [TopologicalSpace H] (G : StructureGroupoid H) : HasGroupoid H G where
  compatible {e e'} he
    he' := by
    rw [chartedSpaceSelf_atlas] at he he'
    simp [he, he', StructureGroupoid.id_mem]

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