pred_covBy

Mathlib.Order.SuccPred.Basic

URI: https://scilib.ai/kg/mathlib#Order.pred_covBy

English

For any a, pred a is covered by a: pred a ⋖ a.

Русский

Для любого a, pred a покрывается перед a: pred a ⋖ a.

LaTeX

$$$$pred(a) \prec a.$$$$

Lean4

theorem pred_covBy (a : α) : pred a ⋖ a :=
  pred_covBy_of_not_isMin <| not_isMin a

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

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

Разделы

Аффилиация

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