English
The C^0 groupoid equals the groupoid of open partial homeomorphisms.
Русский
Группа C^0 совпадает с группойодом открытых частичных гомеморфизмов.
LaTeX
$$$contDiffGroupoid 0 I = continuousGroupoid H$$$
Lean4
/-- The groupoid of `0`-times continuously differentiable maps is just the groupoid of all
open partial homeomorphisms -/
theorem contDiffGroupoid_zero_eq : contDiffGroupoid 0 I = continuousGroupoid H :=
by
apply le_antisymm le_top
intro u
_
-- we have to check that every open partial homeomorphism belongs to `contDiffGroupoid 0 I`,
-- by unfolding its definition
change u ∈ contDiffGroupoid 0 I
rw [contDiffGroupoid, mem_groupoid_of_pregroupoid, contDiffPregroupoid]
simp only [contDiffOn_zero]
constructor
· refine I.continuous.comp_continuousOn (u.continuousOn.comp I.continuousOn_symm ?_)
exact (mapsTo_preimage _ _).mono_left inter_subset_left
· refine I.continuous.comp_continuousOn (u.symm.continuousOn.comp I.continuousOn_symm ?_)
exact (mapsTo_preimage _ _).mono_left inter_subset_left
