mono — Mathlib

English

If mulSupport f' is contained in mulSupport f, then HasCompactMulSupport f' holds whenever HasCompactMulSupport f holds.

Русский

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

LaTeX

$$$\\text{HasCompactMulSupport}(f) \\land (\\operatorname{mulSupport}(f') \\subseteq \\operatorname{mulSupport}(f)) \\Rightarrow \\text{HasCompactMulSupport}(f').$$$

Lean4

@[to_additive]
theorem mono {f' : α → γ} (hf : HasCompactMulSupport f) (hff' : mulSupport f' ⊆ mulSupport f) :
    HasCompactMulSupport f' :=
  hf.mono' <| hff'.trans subset_closure

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