bddAbove_range_of_hasCompactMulSupport

English

If a continuous function has compact support, then its range is bounded above (there exists an upper bound for all its values).

Русский

Если непрерывная функция имеет компактную опору, то её множество значений ограничено сверху.

LaTeX

$$$\\exists M \\in \\alpha\\,\\forall b \\in \\beta:\\, f(b) \\le M$$$

Lean4

/-- A continuous function with compact support is bounded above. -/
@[to_additive /-- A continuous function with compact support is bounded above. -/
    ]
theorem bddAbove_range_of_hasCompactMulSupport [ClosedIciTopology α] [One α] {f : β → α} (hf : Continuous f)
    (h : HasCompactMulSupport f) : BddAbove (range f) :=
  Continuous.bddBelow_range_of_hasCompactMulSupport (α := αᵒᵈ) hf h

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