_aux_Mathlib_Analysis_Distribution_ContDiffMapSupportedIn___macroRules_Distributions_term𝓓^{_}_{_}(_,_)_1

English

If a 𝓓^{n}_{K}-function has compact support, then its support is contained in the compact set K.

Русский

Если функция из класса 𝓓^{n}_{K} имеет компактную опору, то её опора вложена в компактный набор K.

LaTeX

$$$$\\text{HasCompactSupport } f\\Rightarrow \\operatorname{supp} f \\subseteq K.$$$$

Lean4

@[scoped macro Distributions.«term𝓓^{_}_{_}(_,_)»]
public meta def
  «_aux_Mathlib_Analysis_Distribution_ContDiffMapSupportedIn___macroRules_Distributions_term𝓓^{_}_{_}(_,_)_1» :
    Macro✝ := fun
  | `(𝓓^{$n}_{$K}($E, $F)) => ``(ContDiffMapSupportedIn $E $F $n $K)
  | _ => no_error_if_unused% throw✝ Lean.Macro.Exception.unsupportedSyntax✝

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