exists_forall_ge_of_hasCompactMulSupport

English

A continuous function with compact support has a global maximum.

Русский

Непрерывная функция с компактной поддержкой достигает глобального максимума.

LaTeX

$$$\exists x\; \forall y\; f(y) \le f(x)$$$

Lean4

/-- A continuous function with compact support has a global maximum. -/
@[to_additive /-- A continuous function with compact support has a global maximum. -/
    ]
theorem exists_forall_ge_of_hasCompactMulSupport [ClosedIciTopology α] [Nonempty β] [One α] {f : β → α}
    (hf : Continuous f) (h : HasCompactMulSupport f) : ∃ x : β, ∀ y : β, f y ≤ f x :=
  Continuous.exists_forall_le_of_hasCompactMulSupport (α := αᵒᵈ) hf h

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