English
Given a family φ_i of continuous maps on S_i covering α in a neighborhood sense, which agree on overlaps, there exists a global continuous map φ on α that restricts to φ_i on each S_i.
Русский
Дано семейство непрерывных отображений φ_i на подмножестве S_i, чьи домены образуют покрытие α в окрестностном смысле и которые согласованы на пересечениях; существует непрерывное отображение на α, ограничиваемое равными φ_i на каждом S_i.
LaTeX
$$$\\exists F \\in C(\\alpha,\\beta)\\;\\text{such that}\\;F\\restriction S_i = φ_i\\quad(∀ i)$$$
Lean4
/-- A family `φ i` of continuous maps `C(S i, β)`, where the domains `S i` contain a neighbourhood
of each point in `α` and the functions `φ i` agree pairwise on intersections, can be glued to
construct a continuous map in `C(α, β)`. -/
noncomputable def liftCover : C(α, β) :=
haveI H : ⋃ i, S i = Set.univ := Set.iUnion_eq_univ_iff.2 fun x ↦ (hS x).imp fun _ ↦ mem_of_mem_nhds
mk (Set.liftCover S (fun i ↦ φ i) hφ H) <|
continuous_of_cover_nhds hS fun i ↦ by
rw [continuousOn_iff_continuous_restrict]
simpa +unfoldPartialApp only [Set.restrict, Set.liftCover_coe] using map_continuous (φ i)
