div — Mathlib

English

If f and f' have compact multiplicative support, then their quotient f / f' has compact multiplicative support.

Русский

Если f и f' имеют компактную мультиподдержку, то f / f' имеет компактную мультиподдержку.

LaTeX

$$$\\text{HasCompactMulSupport}(f) \\land \\text{HasCompactMulSupport}(f') \\Rightarrow \\text{HasCompactMulSupport}(\\,f / f'\\,).$$$

Lean4

@[to_additive]
theorem div {α β : Type*} [TopologicalSpace α] [DivisionMonoid β] {f f' : α → β} (hf : HasCompactMulSupport f)
    (hf' : HasCompactMulSupport f') : HasCompactMulSupport (f / f') :=
  div_eq_mul_inv f f' ▸ hf.mul hf'.inv

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