dist_pos_of_ne

Mathlib.Data.Nat.Dist

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

← MathLib Explorer

English

If i ≠ j then dist(i,j) > 0.

Русский

Если i ≠ j, то dist(i,j) > 0.

LaTeX

$$$$ i \ne j \Rightarrow 0 < dist(i,j). $$$$

Lean4

theorem dist_pos_of_ne {i j : Nat} (h : i ≠ j) : 0 < dist i j := by
  cases h.lt_or_gt with
  | inl h => rw [dist_eq_sub_of_le h.le]; apply tsub_pos_of_lt h
  | inr h => rw [dist_eq_sub_of_le_right h.le]; apply tsub_pos_of_lt h

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

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

Разделы

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

Аффилиация

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