English
Constructing IsLocalHomeomorphOn from a family of local agreement data.
Русский
Построение IsLocalHomeomorphOn из набора данных локального совпадения.
LaTeX
$$$IsLocalHomeomorphOn\\; f\\; s := \\text{mk from } h : \\forall x\\in s, \\exists e, x\\in e.source \\land f|_{e.source}=e$$$
Lean4
/-- Proves that `f` satisfies `IsLocalHomeomorphOn f s`. The condition `h` is weaker than the
definition of `IsLocalHomeomorphOn f s`, since it only requires `e : OpenPartialHomeomorph X Y` to
agree with `f` on its source `e.source`, as opposed to on the whole space `X`. -/
theorem mk (h : ∀ x ∈ s, ∃ e : OpenPartialHomeomorph X Y, x ∈ e.source ∧ Set.EqOn f e e.source) :
IsLocalHomeomorphOn f s := by
intro x hx
obtain ⟨e, hx, he⟩ := h x hx
exact
⟨{ e with
toFun := f
map_source' := fun _x hx ↦ by rw [he hx]; exact e.map_source' hx
left_inv' := fun _x hx ↦ by rw [he hx]; exact e.left_inv' hx
right_inv' := fun _y hy ↦ by rw [he (e.map_target' hy)]; exact e.right_inv' hy
continuousOn_toFun := (continuousOn_congr he).mpr e.continuousOn_toFun },
hx, rfl⟩
