mulSupport_along_fiber_finite_of_finite

English

If mulSupport f is finite, then so is mulSupport of the fiber map b ↦ f(a,b).

Русский

Если mulSupport f конечно, то и mulSupport для среза по фиксированному a тоже конечно.

LaTeX

$$$$(mulSupport f).Finite \Rightarrow (mulSupport (\lambda b, f(a,b))).Finite.$$$$

Lean4

@[to_additive (attr := simp)]
theorem mulSupport_along_fiber_finite_of_finite (f : α × β → γ) (a : α) (h : (mulSupport f).Finite) :
    (mulSupport fun b ↦ f (a, b)).Finite :=
  (h.image Prod.snd).subset (mulSupport_along_fiber_subset f a)

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