sub_le_iff

Mathlib.Algebra.Group.Fin.Basic

URI: https://scilib.ai/kg/mathlib#Fin.sub_le_iff

English

For Fin(n), a - b ≤ a is equivalent to b ≤ a.

Русский

Для Fin(n) верно, что a − b ≤ a эквивалентно b ≤ a.

LaTeX

$$$\\forall {n},\\forall {a,b}\\in \\mathrm{Fin}(n),\\ a-b \\le a \\iff b \\le a$$$

Lean4

@[simp]
theorem sub_le_iff {n : ℕ} {a b : Fin n} : a - b ≤ a ↔ b ≤ a := by
  rw [← not_iff_not, Fin.not_le, Fin.not_le, lt_sub_iff]

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

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

Разделы

Аффилиация

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