add_one_lt_of_even

Mathlib.Algebra.Group.Nat.Even

URI: https://scilib.ai/kg/mathlib#Nat.add_one_lt_of_even

← MathLib Explorer

English

If m,n are even and n < m, then n+1 < m.

Русский

Если n и m чётны и n < m, то n+1 < m.

LaTeX

$$$\operatorname{Even}(n) \to \operatorname{Even}(m) \to n < m \to n+1 < m$$$

Lean4

theorem add_one_lt_of_even (hn : Even n) (hm : Even m) (hnm : n < m) : n + 1 < m := by
  grind
    -- Here are examples of how `parity_simps` can be used with `Nat`.

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

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

Разделы

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

Аффилиация

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