English
For a given predicate p on α, an element x in P α is LiftP p if and only if x can be written as a pair ⟨a, f⟩ with a in the index data and f assigning to each i a value in α i, and such that p holds for every component f i j.
Русский
Пусть имеется предикат p на α. Элемент x ∈ P α удовлетворяет LiftP p тогда и только тогда, когда x может быть записано как ⟨a, f⟩ с некоторым a, и для каждого i, j выполняется p (f i j).
LaTeX
$$$\\text{LiftP } p\, x \\;\\Longleftrightarrow\\; \\exists a\\, f,\\ x = \\langle a, f \\rangle \\land \\forall i j, p (f i j)$$$
Lean4
theorem liftP_iff {α : TypeVec n} (p : ∀ ⦃i⦄, α i → Prop) (x : P α) :
LiftP p x ↔ ∃ a f, x = ⟨a, f⟩ ∧ ∀ i j, p (f i j) :=
by
constructor
· rintro ⟨y, hy⟩
rcases h : y with ⟨a, f⟩
refine ⟨a, fun i j => (f i j).val, ?_, fun i j => (f i j).property⟩
rw [← hy, h, map_eq]
rfl
rintro ⟨a, f, xeq, pf⟩
use ⟨a, fun i j => ⟨f i j, pf i j⟩⟩
rw [xeq]; rfl
