English
If a complex construction of groupoids is compatible via lifting, the composed groupoid structure still yields a valid HasGroupoid relation on the composed spaces.
Русский
Если сложная конструкция группоида совместима через подъем (lift), то композиция группоида сохраняет корректность отношения HasGroupoid на композиции пространств.
LaTeX
$$$ \forall \{e,e'\} \text{ etc. } \Rightarrow \ HasGroupoid H_3 G_1.$$$
Lean4
theorem mdifferentiableAt_atlas (h : e ∈ atlas H M) {x : M} (hx : x ∈ e.source) : MDifferentiableAt I I e x :=
by
rw [mdifferentiableAt_iff]
refine ⟨(e.continuousOn x hx).continuousAt (e.open_source.mem_nhds hx), ?_⟩
have mem : I ((chartAt H x : M → H) x) ∈ I.symm ⁻¹' ((chartAt H x).symm ≫ₕ e).source ∩ range I := by
simp only [hx, mfld_simps]
have : (chartAt H x).symm.trans e ∈ contDiffGroupoid 1 I := HasGroupoid.compatible (chart_mem_atlas H x) h
have A :
ContDiffOn 𝕜 1 (I ∘ (chartAt H x).symm.trans e ∘ I.symm)
(I.symm ⁻¹' ((chartAt H x).symm.trans e).source ∩ range I) :=
this.1
have B := A.differentiableOn le_rfl (I ((chartAt H x : M → H) x)) mem
simp only [mfld_simps] at B
rw [inter_comm, differentiableWithinAt_inter] at B
· simpa only [mfld_simps]
· apply IsOpen.mem_nhds ((OpenPartialHomeomorph.open_source _).preimage I.continuous_symm) mem.1
