comp_homeomorph — Mathlib

English

If f has compact multiplicative support, then f ∘ φ has compact multiplicative support for a homeomorphism φ.

Русский

Если у функции f есть компактная мультиподдержка, то f ∘ φ имеет компактную мультиподдержку при гомеоморфизме φ.

LaTeX

$$$\operatorname{HasCompactMulSupport}(f) \Rightarrow \operatorname{HasCompactMulSupport}(f \circ \phi).$$$

Lean4

@[to_additive]
theorem comp_homeomorph {M} [One M] {f : Y → M} (hf : HasCompactMulSupport f) (φ : X ≃ₜ Y) :
    HasCompactMulSupport (f ∘ φ) :=
  hf.comp_isClosedEmbedding φ.isClosedEmbedding

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