English
Characterize the membership of a point u in the support of x in terms of the existence of representations a, f with abs ⟨a, f⟩ = x.
Русский
Определение принадлежности точки u поддержке x через существование представления a, f с равенством abs ⟨a, f⟩ = x.
LaTeX
$$$$\forall {F : Type u \to Type v} [q : QPF F] {\alpha : Type u} (x : F \alpha) (u : \alpha), u \in supp x \leftrightarrow \forall a f, abs ⟨a, f⟩ = x \rightarrow u \in f '' univ.$$$$
Lean4
theorem mem_supp {α : Type u} (x : F α) (u : α) : u ∈ supp x ↔ ∀ a f, abs ⟨a, f⟩ = x → u ∈ f '' univ :=
by
rw [supp]; dsimp; constructor
· intro h a f haf
have : Liftp (fun u => u ∈ f '' univ) x := by
rw [liftp_iff]
exact ⟨a, f, haf.symm, fun i => mem_image_of_mem _ (mem_univ _)⟩
exact h this
intro h p; rw [liftp_iff]
rintro ⟨a, f, xeq, h'⟩
rcases h a f xeq.symm with ⟨i, _, hi⟩
rw [← hi]; apply h'
