findGreatest_of_not

Mathlib.Data.Nat.Find

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

English

If not P(n+1), then findGreatest P (n+1) = findGreatest P n.

Русский

Если не выполняется P(n+1), то findGreatest P (n+1) = findGreatest P n.

LaTeX

$$$\\lnot P(n+1) \\Rightarrow \\mathrm{findGreatest}(P,n+1) = \\mathrm{findGreatest}(P,n).$$$

Lean4

@[simp]
theorem findGreatest_of_not (h : ¬P (n + 1)) : findGreatest P (n + 1) = findGreatest P n := by
  simp [Nat.findGreatest, h]

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

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

Разделы

Аффилиация

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