Raised

Mathlib.Data.Ordmap.Invariants

URI: https://scilib.ai/kg/mathlib#Ordnode.Raised

English

Raised(n,m) holds when m is either n or n+1, i.e., m equals n or m equals n+1.

Русский

Raised(n,m) означает, что m равна n или n+1.

LaTeX

$$Raised(n,m) := (m = n) ∨ (m = n + 1)$$

Lean4

/-- `Raised n m` means `m` is either equal or one up from `n`. -/
def Raised (n m : ℕ) : Prop :=
  m = n ∨ m = n + 1

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

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

Разделы

Аффилиация

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