exists_forall_le_of_hasCompactMulSupport

English

If f is continuous on a compact set K, then the image f''K is bounded below.

Русский

Если f непрерывна на компактном множестве K, то образ f(K) ограничен снизу.

LaTeX

$$"BddBelow(f''K)"$$

Lean4

/-- A continuous function with compact support has a global minimum. -/
@[to_additive /-- A continuous function with compact support has a global minimum. -/
    ]
theorem exists_forall_le_of_hasCompactMulSupport [ClosedIicTopology α] [Nonempty β] [One α] {f : β → α}
    (hf : Continuous f) (h : HasCompactMulSupport f) : ∃ x : β, ∀ y : β, f x ≤ f y :=
  by
  obtain ⟨_, ⟨x, rfl⟩, hx⟩ := (h.isCompact_range hf).exists_isLeast (range_nonempty _)
  rw [mem_lowerBounds, forall_mem_range] at hx
  exact ⟨x, hx⟩

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