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 (fun a ↦ f a / g a) = support f ∩ support g := by simp [div_eq_mul_inv]

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