supp_map — Mathlib

English

If q is uniform, then the support of the mapped x by g is the image of the support by g on each coordinate.

Русский

Если q однороден, то опора отображенного x через g равна образу опоры через g по каждой координате.

LaTeX

$$$$ \\mathrm{supp}(g<$$>x)\\;i = g i'' \\mathrm{supp}\ x\\;i. $$$$

Lean4

theorem supp_map (h : q.IsUniform) {α β : TypeVec n} (g : α ⟹ β) (x : F α) (i) : supp (g <$$> x) i = g i '' supp x i :=
  by
  rw [← abs_repr x]; obtain ⟨a, f⟩ := repr x; rw [← abs_map, MvPFunctor.map_eq]
  rw [supp_eq_of_isUniform h, supp_eq_of_isUniform h, ← image_comp]
  rfl

Похожие утверждения