le_min — Mathlib

English

Let m be an element of the extended order and S a finite nonempty subset of the base order. If m ≤ a for all a ∈ S, then m ≤ min S.

Русский

Пусть m принадлежит расширенному порядку, а S — конечное непустое подмножество базового порядка. Если m ≤ a для всех a ∈ S, то m ≤ min S.

LaTeX

$$$$\forall m \in \mathrm{WithTop}(\alpha),\ \forall S \subseteq \alpha,\ S \text{ finite nonempty},\ (\forall a \in S,\ m \le a) \Rightarrow m \le \min S.$$$$

Lean4

protected theorem le_min {m : WithTop α} {s : Finset α} (st : ∀ a : α, a ∈ s → m ≤ a) : m ≤ s.min :=
  Finset.le_inf st

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