isCompact_range_of_mulSupport_subset_isCompact

English

If f has compact multiplicative support and its domain is compactly contained in K, then the image range(f) is compact.

Русский

Если mulSupport(f) поместим в компактный K, то образ range(f) компактен.

LaTeX

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

Lean4

@[to_additive]
theorem _root_.isCompact_range_of_mulSupport_subset_isCompact [TopologicalSpace β] (hf : Continuous f)
    (hk : IsCompact K) (h'f : mulSupport f ⊆ K) : IsCompact (range f) :=
  by
  rcases range_eq_image_or_of_mulSupport_subset h'f with h2 | h2 <;> rw [h2]
  exacts [hk.image hf, (hk.image hf).insert 1]

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