lt_min'_iff

Mathlib.Data.Finset.Max

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

English

For a nonempty finite S, x < min' S iff ∀ y ∈ S, x < y.

Русский

Для непустого конечного S верно: x < min' S тогда и только тогда, когда для каждого y ∈ S выполняется x < y.

LaTeX

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

Lean4

@[simp]
theorem lt_min'_iff : x < s.min' H ↔ ∀ y ∈ s, x < y :=
  @max'_lt_iff αᵒᵈ _ _ H _

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

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

Разделы

Аффилиация

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