max'_le_iff

Mathlib.Data.Finset.Max

URI: https://scilib.ai/kg/mathlib#Finset.max'_le_iff

English

For nonempty S, max' S ≤ x iff ∀ y ∈ S, y ≤ x.

Русский

Для непустого S максимум max' S ≤ x тогда и только тогда, когда для каждого y ∈ S выполняется y ≤ x.

LaTeX

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

Lean4

@[simp]
theorem max'_le_iff {x} : s.max' H ≤ x ↔ ∀ y ∈ s, y ≤ x :=
  isLUB_le_iff (isGreatest_max' s H).isLUB

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

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

Разделы

Аффилиация

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