minimal

Mathlib.Order.Minimal

URI: https://scilib.ai/kg/mathlib#IsLeast.minimal

English

IsLeast s x implies that x is minimal among elements of s, i.e., x is minimal with respect to the predicate of membership in s.

Русский

IsLeast s x означает, что x минимален среди элементов s по отношению к принадлежности x s.

LaTeX

$$$IsLeast\\, s\\, x \\Rightarrow Minimal(\\cdot \\in s)\\, x$$$

Lean4

theorem minimal (h : IsLeast s x) : Minimal (· ∈ s) x :=
  ⟨h.1, fun _b hb _ ↦ h.2 hb⟩

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

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

Разделы

Аффилиация

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