English
LiftP characterizes when a predicate lifts along the functor: LiftP p x holds exactly when x can be represented as abs ⟨a,f⟩ and p holds for all coordinates of f.
Русский
LiftP описывает, когда предикат поднимается вдоль функторa: LiftP p x сохраняется тогда
LaTeX
$$$$ \\mathrm{LiftP}\\; p\\; x \\;\\iff\\; \\exists a,f,\\ x = \\mathrm{abs}\\langle a,f\\rangle \\land \\forall i,j,\\ p(i, f(i,j)). $$$$
Lean4
theorem liftP_iff {α : TypeVec n} (p : ∀ ⦃i⦄, α i → Prop) (x : F α) :
LiftP p x ↔ ∃ a f, x = abs ⟨a, f⟩ ∧ ∀ i j, p (f i j) :=
by
constructor
· rintro ⟨y, hy⟩
rcases h : repr y with ⟨a, f⟩
use a, fun i j => (f i j).val
constructor
· rw [← hy, ← abs_repr y, h, ← abs_map]; rfl
intro i j
apply (f i j).property
rintro ⟨a, f, h₀, h₁⟩
use abs ⟨a, fun i j => ⟨f i j, h₁ i j⟩⟩
rw [← abs_map, h₀]; rfl
