inv — Mathlib

English

If f has compact multiplicative support, then its inverse f^{-1} also has compact multiplicative support.

Русский

Если mulTSupport(f) компактна, то и mulTSupport(f^{-1}) компактна.

LaTeX

$$$\\text{HasCompactMulSupport}(f) \\Rightarrow \\text{HasCompactMulSupport}(f^{-1}).$$$

Lean4

@[to_additive]
protected theorem inv {α β : Type*} [TopologicalSpace α] [DivisionMonoid β] {f : α → β} (hf : HasCompactMulSupport f) :
    HasCompactMulSupport (f⁻¹) := by simpa only [HasCompactMulSupport, mulTSupport, mulSupport_inv] using hf

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