dist_le'

Mathlib.Data.Ordmap.Invariants

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

English

Symmetric distance bound: dist(m,n) ≤ 1 when Raised n m.

Русский

Обратная связность: dist(m,n) ≤ 1 при Raised n m.

LaTeX

$$Raised(n,m) → dist(m,n) ≤ 1$$

Lean4

theorem dist_le' {n m} (H : Raised n m) : Nat.dist m n ≤ 1 := by rw [Nat.dist_comm]; exact H.dist_le

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

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

Разделы

Аффилиация

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