findGreatest_spec — Mathlib

English

If m ≤ n and P m holds, then P(findGreatest P n) holds.

Русский

Если m ≤ n и P(m) верно, то P(findGreatest P n) верно.

LaTeX

$$$(m \le n) \land P m \Rightarrow P(\mathrm{findGreatest} P n).$$$

Lean4

theorem findGreatest_spec (hmb : m ≤ n) (hm : P m) : P (Nat.findGreatest P n) :=
  by
  by_cases h : Nat.findGreatest P n = 0
  · cases m
    · rwa [h]
    exact ((findGreatest_eq_zero_iff.1 h) (zero_lt_succ _) hmb hm).elim
  · exact (findGreatest_eq_iff.1 rfl).2.1 h

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