support_div' — Mathlib

English

Let f, g: I → G₀. Then the support of the pointwise quotient f(a)/g(a) equals the intersection of the supports of f and g.

Русский

Пусть f, g: I → G₀. Тогда опора функции a ↦ f(a)/g(a) равна пересечению опор f и g.

LaTeX

$$$\\operatorname{support}\\bigl(a \\mapsto \\tfrac{f(a)}{g(a)}\\bigr) = \\operatorname{support}(f) \\cap \\operatorname{support}(g)$$$

Lean4

@[simp]
theorem support_div' (f g : ι → G₀) : support (f / g) = support f ∩ support g :=
  support_div _ _

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