minimum_of_length_pos_le_iff — Mathlib

English

For nonempty l and any b, minimum_of_length_pos(l) ≤ b iff minimum(l) ≤ b.

Русский

Для непустого списка и любого b выполняется minimum_of_length_pos(l) ≤ b тогда и только если minimum(l) ≤ b.

LaTeX

$$$\\min\\_of\\_length\\_pos(l) \\le b \\iff \\min(l) \\le b$$$

Lean4

@[simp]
theorem minimum_of_length_pos_le_iff {b : α} (h : 0 < l.length) : minimum_of_length_pos h ≤ b ↔ l.minimum ≤ b :=
  WithTop.untop_le_iff _

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