isMin

Mathlib.Order.SuccPred.Limit

URI: https://scilib.ai/kg/mathlib#Order.IsPredPrelimit.isMin

English

If IsPredPrelimit(pred a) holds, then a is minimal.

Русский

Если IsPredPrelimit(pred a) выполняется, то a минимален.

LaTeX

$$$IsPredPrelimit(\mathrm{pred}(a)) \rightarrow IsMin(a)$$$

Lean4

protected theorem isMin (h : IsPredPrelimit (pred a)) : IsMin a :=
  h.dual.isMax

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

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

Разделы

Аффилиация

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