setOf_minimal_subset

Mathlib.Order.Minimal

URI: https://scilib.ai/kg/mathlib#setOf_minimal_subset

English

The set of elements x that are minimal with respect to membership in s is contained in s itself.

Русский

Множество элементов x, минимальных по отношению к принадлежности x к s, содержится внутри s.

LaTeX

$$$\\{x \\mid Minimal(\\cdot \\in s)\\; x\\} \\subseteq s$$$

Lean4

theorem setOf_minimal_subset (s : Set α) : {x | Minimal (· ∈ s) x} ⊆ s :=
  sep_subset ..

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

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

Разделы

Аффилиация

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