English
If c and p satisfy a lifting condition, then there is a CanLift instance lifting sets via image c '' ·, preserving membership by p.
Русский
Если существуют соответствия между c и p, то существует инстанс CanLift для отображения множеств через изображение c, сохраняющий свойство p на элементах.
LaTeX
$$$\text{(c) (p) [CanLift } \alpha \beta c p] : \text{CanLift} (\operatorname{Set} \alpha) (\operatorname{Set} \beta) (c '' \cdot) (\lambda s \Rightarrow \forall x \in s, p x)$$$
Lean4
instance canLift (c) (p) [CanLift α β c p] : CanLift (Set α) (Set β) (c '' ·) fun s => ∀ x ∈ s, p x where
prf _ hs := subset_range_iff_exists_image_eq.mp fun x hx => CanLift.prf _ (hs x hx)
