min_mem

Mathlib.Order.WellFoundedSet

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

English

If s is well-founded and nonempty, then the minimal element of s is contained in s.

Русский

Если множество s хорошо основано и непусто, то его минимальный элемент принадлежит s.

LaTeX

$$$hs.min\\, hn \\in s$$$

Lean4

theorem min_mem (hs : IsWF s) (hn : s.Nonempty) : hs.min hn ∈ s :=
  (WellFounded.min hs univ (nonempty_iff_univ_nonempty.1 hn.to_subtype)).2

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

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

Разделы

Аффилиация

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