min_le

Mathlib.Order.WellFoundedSet

URI: https://scilib.ai/kg/mathlib#Set.IsWF.min_le

English

For a ∈ s, the minimal element of s is ≤ a.

Русский

Для элемента a ∈ s минимальный элемент s не превосходит a.

LaTeX

$$$hs.min\\, hn \\le a$$$

Lean4

theorem min_le (hs : s.IsWF) (hn : s.Nonempty) (ha : a ∈ s) : hs.min hn ≤ a :=
  le_of_not_gt (hs.not_lt_min hn ha)

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

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

Разделы

Аффилиация

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