minimum_eq_coe_iff — Mathlib

English

Let l be a finite list in a linear order. The minimum 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

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

Lean4

theorem minimum_eq_coe_iff : minimum l = m ↔ m ∈ l ∧ ∀ a ∈ l, m ≤ a :=
  @maximum_eq_coe_iff αᵒᵈ _ _ _

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