supp_map — Mathlib

English

For IsUniform h and any g : α → β, the support of g <$> x is g '' supp x.

Русский

При IsUniform h и любом g : α → β, поддержка g <$> x равна g '' supp x.

LaTeX

$$$$\forall {F : Type u \to Type u} [q : QPF F] (h : q.IsUniform) {\alpha \u \beta : Type u} (g : \alpha \to \beta) (x : F \alpha),\ supp (g <$> x) = g '' supp x.$$$$

Lean4

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

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