English
For a ∈ P.A and f: P.B a ⟹ α, the support of the element ⟨a, f⟩ in P α is the image of f i over univ, i.e., the set of all f i y as y ranges over the entire domain.
Русский
Для элемента ⟨a, f⟩ в P α граница поддержки состоит из изображений f i на все элементы univ в соответствующей координате i.
LaTeX
$$$\\operatorname{supp} (\\langle a, f \\rangle)\\ i = f i''\\;\\operatorname{univ}$$$
Lean4
theorem supp_eq {α : TypeVec n} (a : P.A) (f : P.B a ⟹ α) (i) : @supp.{u} _ P.Obj _ α (⟨a, f⟩ : P α) i = f i '' univ :=
by
ext x; simp only [supp, image_univ, mem_range, mem_setOf_eq]
constructor <;> intro h
· apply @h fun i x => ∃ y : P.B a i, f i y = x
rw [liftP_iff']
intros
exact ⟨_, rfl⟩
· simp only [liftP_iff']
cases h
subst x
tauto
