English
The iUnionLift construction builds a global function from a family of local functions f_i on S_i by selecting an index i for each x in T, provided coherence on overlaps.
Русский
Конструкция iUnionLift строит глобальную функцию из семейства локальных функций f_i на S_i, выбирая индекс i для каждого x ∈ T при условии согласованности на пересечениях.
LaTeX
$$iUnionLift : (S : ι → Set α) → (f : ∀ i, (S i).Elem → β) → (∀ i j x, f i ⟨x, _⟩ = f j ⟨x, _⟩) → (T : Set α) → (T ⊆ iUnion S) → T.Elem → β$$
Lean4
/-- Given a union of sets `iUnion S`, define a function on the Union by defining
it on each component, and proving that it agrees on the intersections. -/
@[nolint unusedArguments]
noncomputable def iUnionLift (S : ι → Set α) (f : ∀ i, S i → β)
(_ : ∀ (i j) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩) (T : Set α) (hT : T ⊆ iUnion S)
(x : T) : β :=
let i := Classical.indefiniteDescription _ (mem_iUnion.1 (hT x.prop))
f i ⟨x, i.prop⟩
