maximum_eq_coe_iff — Mathlib

English

Let l be a finite list in a linear order. The maximum of l equals m if and only if m is in l and every element of l is ≤ m.

Русский

Пусть l — конечный список в линейном порядке. максимум l равен m тогда и только если m ∈ l и каждый элемент l ≤ m.

LaTeX

$$$\\max(l) = m \\iff \\bigl(m \\in l \\land \\forall a \\in l, a \\le m\\bigr)$$$

Lean4

theorem maximum_eq_coe_iff : maximum l = m ↔ m ∈ l ∧ ∀ a ∈ l, a ≤ m :=
  by
  rw [maximum, ← WithBot.some_eq_coe, argmax_eq_some_iff]
  simp only [id_eq, and_congr_right_iff, and_iff_left_iff_imp]
  intro _ h a hal hma
  rw [_root_.le_antisymm hma (h a hal)]

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