dist_le

Mathlib.Data.Ordmap.Invariants

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

English

If n and m are Raised, then their distance is at most 1: dist(n,m) ≤ 1.

Русский

Если n и m удовлетворяют Raised, то расстояние между ними не превосходит 1.

LaTeX

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

Lean4

theorem dist_le {n m} (H : Raised n m) : Nat.dist n m ≤ 1 := by obtain ⟨H1, H2⟩ := raised_iff.1 H;
  rwa [Nat.dist_eq_sub_of_le H1, tsub_le_iff_left]

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

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

Разделы

Аффилиация

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