English
A condition expresses membership of a coordinate in the support: u ∈ supp x i is equivalent to a universal check over representations of x that u lies in the i-th coordinate’s image.
Русский
Условие выражает принадлежность координаты в опоре: u ∈ supp x i эквивалентно общему проверке по представлениям x: u лежит в образе i-й координаты.
LaTeX
$$$$ u \\in \\mathrm{supp}\\ x\\ i \\;\\iff\\; \\forall a\\ f,\\ \\mathrm{abs}\\langle a,f\\rangle = x \\rightarrow u \\in f\\ i''\\, univ. $$$$
Lean4
theorem mem_supp {α : TypeVec n} (x : F α) (i) (u : α i) : u ∈ supp x i ↔ ∀ a f, abs ⟨a, f⟩ = x → u ∈ f i '' univ :=
by
rw [supp]; dsimp; constructor
· intro h a f haf
have : LiftP (fun i u => u ∈ f i '' univ) x := by
rw [liftP_iff]
refine ⟨a, f, haf.symm, ?_⟩
intro i u
exact mem_image_of_mem _ (mem_univ _)
exact h this
grind [liftP_iff]
