canLift' — Mathlib

English

If there is a nonempty fiber over each index, a similar lifting exists from s → α to ι → α for a Finset s without explicit Nonempty hypotheses.

Русский

При наличии непустой волокны над каждым индексом существует аналогичное поднятие из s → α в ι → α для Finset s без явного условия ненулевой мощности.

LaTeX

$$∀ (ι α : Type*) [_ne : Nonempty α] (s : Finset ι), CanLift (s → α) (ι → α) (fun f i => f i) fun _ => True$$

Lean4

instance canLift' (ι α : Type*) [_ne : Nonempty α] (s : Finset ι) :
    CanLift (s → α) (ι → α) (fun f i => f i) fun _ => True :=
  PiFinsetCoe.canLift ι (fun _ => α) s

Похожие утверждения