findGreatest_is_greatest

Mathlib.Data.Nat.Find

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

English

If findGreatest P n < k and k ≤ n, then P k does not hold.

Русский

Если findGreatest P n < k и k ≤ n, то P(k) ложно.

LaTeX

$$$( \mathrm{findGreatest} P n < k ) \land (k \le n) \Rightarrow \neg P k.$$$

Lean4

theorem findGreatest_is_greatest (hk : Nat.findGreatest P n < k) (hkb : k ≤ n) : ¬P k :=
  (findGreatest_eq_iff.1 rfl).2.2 hk hkb

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

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

Разделы

Аффилиация

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