ciInf_set_le — Mathlib

English

If the image f''s of s is bounded below, then for every c ∈ s, iInf over i ∈ s of f(i) ≤ f(c).

Русский

Если образ f''s квадрата s ограничен снизу, то для каждого c ∈ s выполняется iInf_{i∈s} f(i) ≤ f(c).

LaTeX

$$BddBelow(Set.image f s) → ∀ {c} (hc : c ∈ s), iInf (fun i => f i) ≤ f c$$

Lean4

theorem ciInf_set_le {f : β → α} {s : Set β} (H : BddBelow (f '' s)) {c : β} (hc : c ∈ s) : ⨅ i : s, f i ≤ f c :=
  le_ciSup_set (α := αᵒᵈ) H hc

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