mulSupport_of_fiberwise_prod_subset_image

English

For a Finset s and functions f, g, the support of the fiberwise product along g is contained in the image of s under g: mulSupport (λ b, ∏ a ∈ s, if g a = b then f a else 1) ⊆ image g s.

Русский

Для конечного множества s и функций f, g опора волокнистого произведения вдоль g вложится в образ s под g: mulSupport (λ b, ∏ a ∈ s, если g a = b, то f a, иначе 1) ⊆ image g s.

LaTeX

$$$ mulSupport (fun b => ∏ a ∈ s with g a = b, f a) \\subseteq s.image g $$$

Lean4

@[to_additive]
theorem mulSupport_of_fiberwise_prod_subset_image [DecidableEq β] (s : Finset α) (f : α → M) (g : α → β) :
    (mulSupport fun b => ∏ a ∈ s with g a = b, f a) ⊆ s.image g :=
  by
  simp only [Finset.coe_image]
  intro b h
  suffices {a ∈ s | g a = b}.Nonempty by simpa only [fiber_nonempty_iff_mem_image, Finset.mem_image, exists_prop]
  exact Finset.nonempty_of_prod_ne_one h

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