hasCompactSupport — Mathlib

English

There is a CompactlySupportedContinuousMapClass structure on C_c(α,β) rendering it a workable function-like object with map_continuous and hasCompactSupport given by the underlying structure.

Русский

Существует структура CompactlySupportedContinuousMapClass на C_c(α,β), задающая способность работать как объект функций, с map_continuous и hasCompactSupport.

LaTeX

$$CompactlySupportedContinuousMapClass (CompactlySupportedContinuousMap α β) α β$$

Lean4

protected theorem hasCompactSupport (f : C_c(α, β)) : HasCompactSupport f :=
  f.hasCompactSupport'

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