le_ciInf — Mathlib

English

If a is a universal lower bound for f, then a ≤ iInf f.

Русский

Если a является нижной ограничивающей для всех значений f, то a ≤ iInf f.

LaTeX

$$[Nonempty ι] {f : ι → α} {c : α} (H : ∀ x, c ≤ f x) : c ≤ iInf f$$

Lean4

/-- The indexed minimum of a function is bounded below by a uniform lower bound -/
theorem le_ciInf [Nonempty ι] {f : ι → α} {c : α} (H : ∀ x, c ≤ f x) : c ≤ iInf f :=
  ciSup_le (α := αᵒᵈ) H

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