wcovBy_succ

Mathlib.Order.SuccPred.Basic

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

English

Every element a is weakly covered by its successor succ(a).

Русский

Каждый элемент a слабо покрывается своим переходом к succ(a).

LaTeX

$$$a \\mathrel{\\mathrm{WCovBy}} \\operatorname{succ}(a)$$$

Lean4

theorem wcovBy_succ (a : α) : a ⩿ succ a :=
  ⟨le_succ a, fun _ hb => (succ_le_of_lt hb).not_gt⟩

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

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

Разделы

Аффилиация

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