findGreatest_of_ne_zero

Mathlib.Data.Nat.Find

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

English

If findGreatest P n = m and m ≠ 0, then P m holds.

Русский

Если findGreatest P n = m и m ≠ 0, то P m истинно.

LaTeX

$$$\mathrm{findGreatest} P n = m \Rightarrow m \neq 0 \Rightarrow P m.$$$

Lean4

theorem findGreatest_of_ne_zero (h : Nat.findGreatest P n = m) (h0 : m ≠ 0) : P m :=
  (findGreatest_eq_iff.1 h).2.1 h0

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

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

Разделы

Аффилиация

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