English
There is a canonical lifting of a family of types indexed by elements of a finite index set s into a family indexed by all indices, respecting the inclusion of s.
Русский
Существует каноническое отображение/перенос семей типов, индексированных элементами конечного множества s, в семейство индексов по всем индексам, сохраняя включение s.
LaTeX
$$∀ (ι : Type*) (α : ι → Type*) [_ne : ∀ i, Nonempty (α i)] (s : Finset ι), CanLift (∀ i : s, α i) (∀ i, α i) (fun f i => f i) fun _ => True$$
Lean4
instance canLift (ι : Type*) (α : ι → Type*) [_ne : ∀ i, Nonempty (α i)] (s : Finset ι) :
CanLift (∀ i : s, α i) (∀ i, α i) (fun f i => f i) fun _ => True :=
PiSubtype.canLift ι α (· ∈ s)
