mulSupport_along_fiber_subset — Mathlib

English

For f: ι × κ → M and a fixed i, the mulSupport of the fiber map j ↦ f(i, j) is contained in the image of Prod.snd applied to mulSupport f.

Русский

Для f: ι×κ → M и фиксированного i опора вдоль волокна j ↦ f(i, j) содержится в образе Prod.snd применительно к mulSupport f.

LaTeX

$$$ \operatorname{mulSupport}\bigl(j \mapsto f(i,j)\bigr) \subseteq ( \operatorname{mulSupport} f ).\mathrm{image} (\mathrm{Prod}.\mathrm{snd}) $$$

Lean4

@[to_additive]
theorem mulSupport_along_fiber_subset (f : ι × κ → M) (i : ι) :
    (mulSupport fun j ↦ f (i, j)) ⊆ (mulSupport f).image Prod.snd := fun j hj ↦ ⟨(i, j), by simpa using hj⟩

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