instCompactlySupportedContinuousMapClass

English

If f is a CompactlySupportedContinuousMap, then HasCompactSupport f holds (i.e., f has compact support).

Русский

Если f является компактно поддерживаемым непрерывным отображением, то у него имеет компактную опору.

LaTeX

$$HasCompactSupport (CompactlySupportedContinuousMap.instFunLike.coe f)$$

Lean4

instance : CompactlySupportedContinuousMapClass C_c(α, β) α β
    where
  map_continuous f := f.continuous_toFun
  hasCompactSupport f := f.hasCompactSupport'

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