English
If IsUniform holds, then Liftp p x is equivalent to ∀ u ∈ supp x, p u.
Русский
Если IsUniform выполняется, то Liftp p x эквивалентно ∀ u ∈ supp x, p u.
LaTeX
$$$$\forall {F : Type u \to Type u} [q : QPF F] \(h : q.IsUniform) {\alpha : Type u} (x : F \alpha) (p : \alpha \to Prop),\ Liftp p x \leftrightarrow \forall u \in supp x, p u.$$$$
Lean4
theorem liftp_iff_of_isUniform (h : q.IsUniform) {α : Type u} (x : F α) (p : α → Prop) :
Liftp p x ↔ ∀ u ∈ supp x, p 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 ⟨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⟩
