setOf_maximal_subset

Mathlib.Order.Minimal

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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