le_min_iff — Mathlib

English

For m in WithTop α and finite nonempty S, m ≤ min S iff ∀ a ∈ S, m ≤ a.

Русский

Для m из WithTop α и конечного непустого множества S верно: m ≤ min S тогда и только тогда, когда для всех a ∈ S выполняется m ≤ a.

LaTeX

$$$$m \le \min S \iff \forall a \in S,\ m \le a.$$$$

Lean4

@[simp]
protected theorem le_min_iff {m : WithTop α} {s : Finset α} : m ≤ s.min ↔ ∀ a ∈ s, m ≤ a :=
  Finset.le_inf_iff

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