English
If x ∈ S_i, then liftCover S f hf hS x = f_i ⟨x, hx⟩. This provides the expected compatibility of liftCover with the components.
Русский
Если x ∈ S_i, то liftCover S f hf hS x = f_i ⟨x, hx⟩. Это демонстрирует совместимость liftCover с компонентами.
LaTeX
$$$\forall i, \forall x\in S_i:\ liftCover(S,f,hf,hS)(x) = f_i(\langle x, hx\rangle).$$$
Lean4
/-- Glue together functions defined on each of a collection `S` of sets that cover a type. See
also `Set.iUnionLift`. -/
noncomputable def liftCover (S : ι → Set α) (f : ∀ i, S i → β)
(hf : ∀ (i j) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩) (hS : iUnion S = univ) (a : α) :
β :=
iUnionLift S f hf univ hS.symm.subset ⟨a, trivial⟩
