English
For a functor P and predicate p, Liftp p x holds exactly when x can be decomposed as ⟨a, f⟩ with ∀ i, p (f i).
Русский
Для функторa P и предиката p, Liftp p x выполняется тогда и только тогда, когда x можно разложить как ⟨a, f⟩ и ∀ i, p (f i).
LaTeX
$$$\operatorname{Liftp} p x \iff \exists a\ f, x = \langle a, f\rangle \land \forall i, p (f i).$$$
Lean4
theorem liftp_iff {α : Type u} (p : α → Prop) (x : P α) : Liftp p x ↔ ∃ a f, x = ⟨a, f⟩ ∧ ∀ i, p (f i) :=
by
constructor
· rintro ⟨y, hy⟩
rcases h : y with ⟨a, f⟩
refine ⟨a, fun i => (f i).val, ?_, fun i => (f i).property⟩
rw [← hy, h, map_eq_map, PFunctor.map_eq]
congr
rintro ⟨a, f, xeq, pf⟩
use ⟨a, fun i => ⟨f i, pf i⟩⟩
rw [xeq]; rfl
