min_bi_le — Mathlib

English

For a finite, nonempty index set α and a function b: α → ℝ, b(min_bi b) ≤ b(i) for all i in α.

Русский

Для конечного непустого множества индексов α и функции b: α → ℝ верно b(min_bi b) ≤ b(i) для каждого i ∈ α.

LaTeX

$$$\\forall i \\in \\alpha,\\; b(\\min\\_bi b) \\le b(i)$$$

Lean4

@[aesop safe apply]
theorem min_bi_le {b : α → ℝ} (i : α) : b (min_bi b) ≤ b i :=
  Classical.choose_spec (Finite.exists_min b) i

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