English
There is a CanLift structure for Finset.image induced from CanLift β α along c: this lifts predicates on β to predicates on Finset β via image c.
Русский
Существует структура CanLift для Finset.image, выведенная из CanLift β α вдоль c: она поднимает предикаты с β к предикатам на Finset β через образ c.
LaTeX
$$$\\text{CanLift}(\\mathsf{Finset}\\,\\beta, \\mathsf{Finset}\\,\\alpha, \\mathsf{Finset.image}\\; c) \\;\\text{(предикат)}$$$
Lean4
instance canLift (c) (p) [CanLift β α c p] : CanLift (Finset β) (Finset α) (image c) fun s => ∀ x ∈ s, p x where
prf := by
rintro ⟨⟨l⟩, hd : l.Nodup⟩ hl
lift l to List α using hl
exact ⟨⟨l, hd.of_map _⟩, ext fun a => by simp⟩
