English
If q is uniform, then LiftP p x is equivalent to the universal condition on supp x, namely p(i,u) for all i and u ∈ supp x i.
Русский
Если q однороден, то LiftP p x эквивалентно общему условию по опоре: p(i,u) для всех i и всех u в supp x i.
LaTeX
$$$$ \\text{LiftP p x} \\iff \\forall i, \\forall u \\in \\mathrm{supp} x i,\\ p(i,u). $$$$
Lean4
theorem liftP_iff_of_isUniform (h : q.IsUniform) {α : TypeVec n} (x : F α) (p : ∀ i, α i → Prop) :
LiftP p x ↔ ∀ (i), ∀ u ∈ supp x i, p i u :=
by
rw [liftP_iff, ← abs_repr x]
obtain ⟨a, f⟩ := repr x; constructor
· rintro ⟨a', f', abseq, hf⟩ u
rw [supp_eq_of_isUniform h, h _ _ _ _ abseq]
rintro b ⟨i, _, hi⟩
rw [← hi]
apply hf
intro h'
refine ⟨a, f, rfl, fun _ i => h' _ _ ?_⟩
rw [supp_eq_of_isUniform h]
exact ⟨i, mem_univ i, rfl⟩
