max'_le

Mathlib.Data.Finset.Max

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

English

If every y ∈ S satisfies y ≤ x, then max' S ≤ x.

Русский

Если каждый элемент y ∈ S удовлетворяет y ≤ x, то max' S ≤ x.

LaTeX

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

Lean4

theorem max'_le (x) (H2 : ∀ y ∈ s, y ≤ x) : s.max' H ≤ x :=
  H2 _ <| max'_mem _ _

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

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

Разделы

Аффилиация

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