lt_sInf_iff_of_continuous — Mathlib

English

For a nonempty compact set K and a function f continuous on K, for any y in the order, y < sInf(f''K) iff ∀ x ∈ K, y < f(x).

Русский

Для непустого компактного множества K и непрерывной на K функции f, для любого y выполняется: y < sInf(f''K) тогда и только тогда, когда для всех x ∈ K выполняется y < f(x).

LaTeX

$$$y < sInf(f''K) \\iff \\forall x \\in K:\\, y < f(x)$$$

Lean4

theorem lt_sInf_iff_of_continuous [ClosedIicTopology α] {f : β → α} {K : Set β} (hK : IsCompact K) (h0K : K.Nonempty)
    (hf : ContinuousOn f K) (y : α) : y < sInf (f '' K) ↔ ∀ x ∈ K, y < f x :=
  IsCompact.sSup_lt_iff_of_continuous (α := αᵒᵈ) hK h0K hf y

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