iInf_nonpos — Mathlib

English

If there exists i with f(i) ≤ 0, then ⨅ i, f(i) ≤ 0.

Русский

Если существует i, такое что f(i) ≤ 0, тогда ⨅ i, f(i) ≤ 0.

LaTeX

$$$\\exists i, f(i) \\le 0 \\Rightarrow \\inf_{i} f(i) \\le 0$$$

Lean4

/-- As `⨅ i, f i = 0` when the domain of the real-valued function `f` is empty or unbounded below,
it suffices to show that all values of `f` are nonpositive to show that `0 ≤ ⨅ i, f i`. -/
theorem iInf_nonpos (hf : ∀ i, f i ≤ 0) : ⨅ i, f i ≤ 0 :=
  sInf_nonpos <| Set.forall_mem_range.2 hf

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