English
If there is a lifting from α to β with a predicate p, then there is a lifting from List α to List β via List.map c, with the property that for every list l, ∀ x ∈ l, p x holds.
Русский
Если существует отображение-восстановление (lifting) из α в β с предикатом p, то существует отображение-восстановление из List α в List β через List.map c, такое что для каждого списка l выполняется ∀ x ∈ l, p x.
LaTeX
$$$\\mathrm{CanLift}(\\mathrm{List}\\,\\alpha, \\mathrm{List}\\,\\beta, \\mathrm{List.map}\\,c, \\lambda l. \\forall x \\in l,\n p(x)).$$$
Lean4
/-- If each element of a list can be lifted to some type, then the whole list can be
lifted to this type. -/
instance canLift (c) (p) [CanLift α β c p] : CanLift (List α) (List β) (List.map c) fun l => ∀ x ∈ l, p x where
prf l
H := by
rw [← Set.mem_range, Set.range_list_map]
exact fun a ha => CanLift.prf a (H a ha)
