hasCompactMulSupport_iff_eventuallyEq

English

For a function f, the image of its domain under f is compact provided f is continuous, the compact set K exists, and mulSupport f is contained in K. More formally, if f is continuous, K is compact, and mulSupport f ⊆ K, then range(f) is compact.

Русский

Пусть f непрерывна, K компактно и mulSupport(f) ⊆ K; тогда образ диапазона f ∈ β является компактным.

LaTeX

$$$\\text{Continuous}(f) \\land \\operatorname{IsCompact}(K) \\land (\\operatorname{mulSupport}(f) \\subseteq K) \\Rightarrow \\operatorname{IsCompact}(\\operatorname{range}(f)).$$$

Lean4

@[to_additive]
theorem _root_.hasCompactMulSupport_iff_eventuallyEq : HasCompactMulSupport f ↔ f =ᶠ[coclosedCompact α] 1 :=
  mem_coclosedCompact_iff.symm

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