English
A continuous map on a compact space has automatically compact support; this yields a CompactlySupportedContinuousMapClass for G α β when α is compact.
Русский
Любая непрерывная функция на компактном пространстве имеет автоматически компактную опору; это порождает класс CompactlySupportedContinuousMapClass G α β, когда α компактно.
LaTeX
$$$$ \text{If } \alpha \text{ is compact and } G \text{ is a class of maps } α \to β, \text{ then } G \text{ is a CompactlySupportedContinuousMapClass } G α β. $$$$
Lean4
/-- A continuous function on a compact space has automatically compact support. This is not an
instance to avoid type class loops. -/
theorem of_compactSpace (G : Type*) [FunLike G α β] [ContinuousMapClass G α β] [CompactSpace α] :
CompactlySupportedContinuousMapClass G α β
where
map_continuous := map_continuous
hasCompactSupport := by
intro f
exact HasCompactSupport.of_compactSpace f
