bddBelow_range_of_hasCompactMulSupport

English

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

Русский

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

LaTeX

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

Lean4

/-- A continuous function with compact support is bounded below. -/
@[to_additive /-- A continuous function with compact support is bounded below. -/
    ]
theorem bddBelow_range_of_hasCompactMulSupport [ClosedIicTopology α] [One α] {f : β → α} (hf : Continuous f)
    (h : HasCompactMulSupport f) : BddBelow (range f) :=
  (h.isCompact_range hf).bddBelow

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