le_min'_iff

Mathlib.Data.Finset.Max

URI: https://scilib.ai/kg/mathlib#Finset.le_min'_iff

English

For a nonempty finite set S, x ≤ min'(H) iff ∀ y ∈ S, x ≤ y.

Русский

Для непустого конечного множества S верно: x ≤ min'(H) тогда и только тогда, когда ∀ y ∈ S, x ≤ y.

LaTeX

$$$$x \le s.min'(H) \iff \forall y \in s,\ x \le y.$$$$

Lean4

@[simp]
theorem le_min'_iff {x} : x ≤ s.min' H ↔ ∀ y ∈ s, x ≤ y :=
  le_isGLB_iff (isLeast_min' s H).isGLB

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru