English
A generalized gluing construction LiftCover' glues a family F on sets from A into a global map on α, given pairwise coherence.
Русский
Обобщенная конструкция склейки LiftCover' объединяет семейство F, заданное на множествах из A, в глобальное отображение на α при условии парной согласованности.
LaTeX
$$$\\mathrm{liftCover}'\\ A\\ F\\ hF\\ hA \\in C(\\alpha,\\beta)$$$
Lean4
/-- A family `F s` of continuous maps `C(s, β)`, where (1) the domains `s` are taken from a set `A`
of sets in `α` which contain a neighbourhood of each point in `α` and (2) the functions `F s` agree
pairwise on intersections, can be glued to construct a continuous map in `C(α, β)`. -/
noncomputable def liftCover' : C(α, β) :=
let F : ∀ i : A, C(i, β) := fun i => F i i.prop
liftCover ((↑) : A → Set α) F (fun i j => hF i i.prop j j.prop) fun x =>
let ⟨s, hs, hsx⟩ := hA x;
⟨⟨s, hs⟩, hsx⟩
