lt_succ_iff_le

Mathlib.Logic.Denumerable

URI: https://scilib.ai/kg/mathlib#Nat.Subtype.lt_succ_iff_le

← MathLib Explorer

English

For any x,y ∈ s, x < succ y iff x ≤ y.

Русский

Для любых x,y ∈ s верно: x < succ(y) тогда и только тогда, когда x ≤ y.

LaTeX

$$$\forall {x,y\in s},\ x

Lean4

theorem lt_succ_iff_le {x y : s} : x < succ y ↔ x ≤ y :=
  ⟨fun h => le_of_not_gt fun h' => not_le_of_gt h (succ_le_of_lt h'), fun h => lt_of_le_of_lt h (lt_succ_self _)⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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