English
A characterization: (∀ p, Liftp p x ↔ ∀ u ∈ supp x, p u) is equivalent to the existence of a representation a, f of x with a certain subset condition between f and any other representation f'.
Русский
Характеризация: (∀ p, Liftp p x ↔ ∀ u ∈ supp x, p u) эквивалентно существованию представления a, f для x, обладающего условием подмножеств между f и любым другим представлением f'.
LaTeX
$$$$\forall {F : Type u \to Type u} [q : QPF F] {\alpha : Type u} (x : F \alpha), (\forall p, Liftp p x \leftrightarrow \forall u \in supp x, p u) \leftrightarrow \exists a f, abs \langle a, f \rangle = x \land \forall a' f', abs \langle a', f' \rangle = x \rightarrow f '' univ \subseteq f' '' univ.$$$$
Lean4
theorem has_good_supp_iff {α : Type u} (x : F α) :
(∀ p, Liftp p x ↔ ∀ u ∈ supp x, p u) ↔ ∃ a f, abs ⟨a, f⟩ = x ∧ ∀ a' f', abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ :=
by
constructor
· intro h
have : Liftp (supp x) x := by rw [h]; intro u; exact id
rw [liftp_iff] at this
rcases this with ⟨a, f, xeq, h'⟩
refine ⟨a, f, xeq.symm, ?_⟩
intro a' f' h''
rintro u ⟨i, _, hfi⟩
have : u ∈ supp x := by rw [← hfi]; apply h'
exact (mem_supp x u).mp this _ _ h''
rintro ⟨a, f, xeq, h⟩ p; rw [liftp_iff]; constructor
· rintro ⟨a', f', xeq', h'⟩ u usuppx
rcases (mem_supp x u).mp usuppx a' f' xeq'.symm with ⟨i, _, f'ieq⟩
rw [← f'ieq]
apply h'
intro h'
refine ⟨a, f, xeq.symm, ?_⟩; intro i
apply h'; rw [mem_supp]
intro a' f' xeq'
apply h a' f' xeq'
apply mem_image_of_mem _ (mem_univ _)
