max_bi_le — Mathlib

English

Let α be a nonempty finite set and b: α → ℝ. Then for every i ∈ α, b(i) is at most the maximum value of b over α, i.e. b(i) ≤ max_{j∈α} b(j).

Русский

Пусть α — ненулевой конечный множество и задана функция b: α → ℝ. Тогда для каждого i ∈ α выполняется b(i) ≤ max_{j∈α} b(j).

LaTeX

$$$\forall i\in\alpha:\; b(i) \le \max_{j\in\alpha} b(j)$$$

Lean4

@[aesop safe apply]
theorem max_bi_le {b : α → ℝ} (i : α) : b i ≤ b (max_bi b) :=
  Classical.choose_spec (Finite.exists_max b) i

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