isCompact_range — Mathlib

English

If a function f has HasCompactMulSupport, and it is continuous, then its range is compact.

Русский

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

LaTeX

$$$\\text{HasCompactMulSupport}(f) \\land \\text{Continuous}(f) \\Rightarrow \\operatorname{IsCompact}(\\operatorname{range}(f)).$$$

Lean4

@[to_additive]
theorem isCompact_range [TopologicalSpace β] (h : HasCompactMulSupport f) (hf : Continuous f) : IsCompact (range f) :=
  isCompact_range_of_mulSupport_subset_isCompact hf h (subset_mulTSupport f)

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